From 5f562d7ac9540b684f331a5d76d44c96c1260b3d Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 10 Mar 2024 00:19:27 +0000
Subject: [PATCH] no sorry in qam_A_example

---
 src/linear_algebra/blackbox.lean              | 215 +++++++-------
 src/linear_algebra/kronecker_to_tensor.lean   |  18 +-
 src/linear_algebra/my_matrix/basic.lean       |  20 +-
 .../my_matrix/is_almost_hermitian.lean        |   6 -
 src/linear_algebra/my_matrix/spectra.lean     | 130 +++++++++
 src/preq/equiv.lean                           |  15 +
 src/quantum_graph/qam_A_example.lean          | 270 +++++++++++++-----
 7 files changed, 462 insertions(+), 212 deletions(-)
 create mode 100644 src/preq/equiv.lean

diff --git a/src/linear_algebra/blackbox.lean b/src/linear_algebra/blackbox.lean
index 5caed6caf2..715c55cc30 100644
--- a/src/linear_algebra/blackbox.lean
+++ b/src/linear_algebra/blackbox.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Monica Omar
 -/
 import linear_algebra.inner_aut
+import linear_algebra.my_matrix.spectra
+import preq.equiv
 
 /-!
 
@@ -14,134 +16,119 @@ This file contains a blackbox theorem that says that two almost-Hermitian matric
 -/
 
 open_locale big_operators
-lemma equiv.perm.to_pequiv.to_matrix_mem_unitary_group {n : Type*} [decidable_eq n]
-  [fintype n] {𝕜 : Type*} [is_R_or_C 𝕜] [decidable_eq 𝕜] (σ : equiv.perm n) :
-  (equiv.to_pequiv σ).to_matrix ∈ matrix.unitary_group n 𝕜 :=
+
+lemma ite_eq_ite_iff {α : Type*} (a b c : α) :
+  (∀ {p : Prop} [decidable p], @ite α p _inst_1 a c = @ite α p _inst_1 b c)
+    ↔ a = b := by
+{ split; intros h,
+  { specialize @h true _,
+    simp_rw [if_true] at h,
+    exact h, },
+  { simp_rw [h, eq_self_iff_true, forall_2_true_iff], }, }
+
+lemma ite_eq_ite_iff_of_pi {n α : Type*} [decidable_eq n] (a b c :  n → α) :
+  (∀ (i j : n), ite (i = j) (a i) (c i) = ite (i = j) (b i) (c i))
+    ↔ a = b :=
 begin
-  simp_rw [matrix.mem_unitary_group_iff, ← matrix.ext_iff, matrix.mul_eq_mul,
-    matrix.mul_apply, pequiv.to_matrix_apply, boole_mul, equiv.to_pequiv_apply,
-    matrix.one_apply, option.mem_def, matrix.star_apply, pequiv.to_matrix_apply,
-    star_ite, is_R_or_C.star_def, map_one, map_zero, finset.sum_ite_eq,
-    finset.mem_univ, if_true],
-  intros i j,
-  simp_rw [equiv.to_pequiv_apply, option.mem_def, eq_comm, function.injective.eq_iff
-    (equiv.injective _)],
+  rw [← ite_eq_ite_iff _ _ c],
+  simp_rw [function.funext_iff, ite_apply],
+  split; rintros h _ _,
+  { intros i,
+    specialize h i i,
+    simp_rw [eq_self_iff_true, if_true] at h,
+    rw h, },
+  { exact h _, },
 end
 
-def multiset.of_list {α : Type*} : list α → multiset α :=
-  quot.mk _
-
--- instance {α : Type*} : has_coe (list α) (multiset α) :=
---   ⟨of_list⟩
-
 namespace matrix
 
 open_locale matrix
 
 variables {n 𝕜 : Type*} [is_R_or_C 𝕜] [fintype n] [decidable_eq n]
 
-noncomputable def is_hermitian.eigenvalues_multiset [decidable_eq 𝕜]
-  {A : matrix n n 𝕜} (hA : A.is_hermitian) :
-  multiset ℝ :=
-multiset.of_list (list.of_fn (hA.eigenvalues₀))
-
--- example [decidable_eq 𝕜]
---   {A B : matrix n n 𝕜} (hA : A.is_hermitian) (hB : B.is_hermitian) :
---   hA.eigenvalues_multiset = hB.eigenvalues_multiset :=
--- begin
---   ext,
---   congr,
--- end
-
--- example {n : ℕ} {A₁ : fin n → 𝕜} :
---   (multiset.of_list (list.of_fn A₁)) =
-
--- def eq_sets_with_multiplicities {n : ℕ} [decidable_eq 𝕜] (A₁ A₂ : fin n → 𝕜) :
---   -- (∀ (x : 𝕜), (∃ (i : fin n), A₁ i = x) ↔ ∃ (i : fin n), A₂ i = x)
---   -- ∧
---   -- -- (multiset.of_list (list.of_fn A₁))
---   ∀ i, multiset.count (finset.univ.val.map A₁) i = multiset.count (finset.univ.val.map A₂) i :=
--- begin
-  
---   simp only [finset.univ],
--- end
-
-/-- TODO: change this to say equal spectra with same multiplicities. -/
+lemma is_almost_hermitian.spectra_ext [decidable_eq 𝕜]
+  {A B : n → 𝕜} (hA : (diagonal A).is_almost_hermitian)
+  (hB : (diagonal B).is_almost_hermitian) :
+  hA.spectra = hB.spectra
+  ↔ ∃ σ : equiv.perm n, ∀ i, A i = B (σ i) :=
+begin
+  sorry
+end
+
 lemma is_diagonal.spectrum_eq_iff_rotation [decidable_eq 𝕜]
-  (A₁ A₂ : n → 𝕜) :
-  spectrum 𝕜 (diagonal A₁ : matrix n n 𝕜).to_lin'
-    = spectrum 𝕜 (diagonal A₂ : matrix n n 𝕜).to_lin'
+  (A₁ A₂ : n → 𝕜) (hA₁ : (diagonal A₁).is_almost_hermitian) (hA₂ : (diagonal A₂).is_almost_hermitian) :
+  hA₁.spectra = hA₂.spectra
     ↔ ∃ (U : equiv.perm n), diagonal A₂ = inner_aut
       ⟨(equiv.to_pequiv U).to_matrix, equiv.perm.to_pequiv.to_matrix_mem_unitary_group U⟩⁻¹
       (diagonal A₁) :=
 begin
+  simp_rw [inner_aut_apply', unitary_group.inv_apply, ← matrix.ext_iff,
+    mul_apply, star_apply, ← unitary_group.star_coe_eq_coe_star,
+    unitary_group.inv_apply, star_star, unitary_group.coe_mk, pequiv.equiv_to_pequiv_to_matrix,
+    diagonal_apply, mul_ite, mul_zero, finset.sum_ite_eq', finset.mem_univ, if_true,
+    one_apply, mul_boole, star_ite, star_one, star_zero, boole_mul],
+  simp_rw [← ite_and, and_comm, ite_and, ← equiv.eq_symm_apply, finset.sum_ite_eq',
+    finset.mem_univ, if_true, (equiv.injective _).eq_iff],
+  rw [is_almost_hermitian.spectra_ext hA₁ hA₂],
+  simp_rw [ite_eq_ite_iff_of_pi, function.funext_iff],
   split,
-  { simp_rw [inner_aut_apply', unitary_group.inv_apply, ← matrix.ext_iff,
-      mul_apply, star_apply, ← unitary_group.star_coe_eq_coe_star,
-      unitary_group.inv_apply, star_star, unitary_group.coe_mk, pequiv.equiv_to_pequiv_to_matrix,
-      diagonal_apply, mul_ite, mul_zero, finset.sum_ite_eq', finset.mem_univ, if_true,
-      one_apply, mul_boole, star_ite, star_one, star_zero, boole_mul],
-    simp_rw [← ite_and, and_comm, ite_and, ← equiv.eq_symm_apply, finset.sum_ite_eq',
-      finset.mem_univ, if_true, (equiv.injective _).eq_iff, diagonal.spectrum, set.ext_iff,
-      set.mem_set_of_eq],
-    intros h,
-    simp_rw [ite_eq_iff', @eq_comm _ _ (ite _ _ _), ite_eq_iff', eq_self_iff_true,
-      imp_true_iff, and_true, forall_and_distrib],
-    let H : ∀ i j, ((i = j → ¬i = j → 0 = A₂ i) ↔ true),
-    { intros i j,
-      split,
-      { simp_rw [imp_true_iff], },
-      { intros H h1 h2,
-        contradiction, }, },
-    simp only [H, and_true],
-    have H' : ∀ (U : equiv.perm n) i j, (¬i = j → i = j → A₁ ((equiv.symm U) i) = 0) ↔ true,
-    { intros U i j,
-      split,
-      { simp_rw [imp_true_iff], },
-      { intros H h1 h2,
-        contradiction, }, },
-    simp only [H', and_true],
-    clear H H',
-    have : ∀ (U : equiv.perm n), (∀ (i j : n), (i = j → i = j → A₁ ((equiv.symm U) i) = A₂ i)) ↔
-       (∀ i, A₁ (equiv.symm U i) = A₂ i),
-    { intros U,
-      split,
-      { intros h i,--intros U i j,
-        exact h i i rfl rfl, },
-      { intros h i j h1 h2,
-        exact h _, }, },
-    simp only [this],
-    clear this,
-    sorry, },
+  { rintros ⟨σ, hσ⟩,
+    use σ,
+    intros i,
+    rw [hσ, equiv.apply_symm_apply], },
   { rintros ⟨U, hU⟩,
-    simp_rw [hU, inner_aut.spectrum_eq], },
+    use U,
+    intros i,
+    rw [hU, equiv.symm_apply_apply], },
+end
+
+lemma is_almost_hermitian.spectra_of_inner_aut [decidable_eq 𝕜]
+  {A : matrix n n 𝕜} (hA : A.is_almost_hermitian) (U : unitary_group n 𝕜) :
+  (hA.of_inner_aut U).spectra = hA.spectra :=
+begin
+  sorry
+end
+lemma is_almost_hermitian.inner_aut_spectra [decidable_eq 𝕜]
+  {A : matrix n n 𝕜}
+  (U : unitary_group n 𝕜)
+  (hA : (inner_aut U A).is_almost_hermitian) :
+  hA.spectra = ((is_almost_hermitian_iff_of_inner_aut _).mpr hA).spectra :=
+begin
+  rw ← is_almost_hermitian.spectra_of_inner_aut _ U⁻¹,
+  simp_rw [inner_aut_inv_apply_inner_aut_self],
 end
 
-lemma is_almost_hermitian.spectrum_eq_iff [decidable_eq 𝕜] [linear_order n] {A₁ A₂ : matrix n n 𝕜}
+
+lemma is_almost_hermitian.spectrum_eq_iff [decidable_eq 𝕜] {A₁ A₂ : matrix n n 𝕜}
   (hA₁ : A₁.is_almost_hermitian) (hA₂ : A₂.is_almost_hermitian) :
-  spectrum 𝕜 A₁.to_lin' = spectrum 𝕜 A₂.to_lin'
-    ↔ ∃ (U : unitary_group n 𝕜), A₂ = inner_aut U⁻¹ A₁ :=
+  hA₁.spectra = hA₂.spectra ↔ ∃ (U : unitary_group n 𝕜), A₂ = inner_aut U⁻¹ A₁ :=
 begin
-  rcases hA₁.schur_decomp with ⟨D₁, U₁, h₁⟩,
-  rcases hA₂.schur_decomp with ⟨D₂, U₂, h₂⟩,
-  rcases hA₁ with ⟨α₁, N₁, hA₁⟩,
-  rcases hA₂ with ⟨α₂, N₂, hA₂⟩,
-  rw [← h₁, ← h₂],
-  rw [inner_aut_eq_iff] at h₁ h₂,
   split,
-  { intros h,
-    simp_rw inner_aut.spectrum_eq at h,
-    obtain ⟨σ, hσ⟩ : ∃ σ : equiv.perm n, diagonal D₂
-      = inner_aut ⟨(equiv.to_pequiv σ).to_matrix, _⟩⁻¹ (diagonal D₁) :=
-    (is_diagonal.spectrum_eq_iff_rotation D₁ D₂).mp h,
-    let P : unitary_group n 𝕜 := ⟨(equiv.to_pequiv σ).to_matrix,
-      equiv.perm.to_pequiv.to_matrix_mem_unitary_group σ⟩,
-    existsi U₁ * P * U₂⁻¹,
-    simp_rw [← linear_map.comp_apply, inner_aut_comp_inner_aut, h₁,
-      _root_.mul_inv_rev, inv_inv, mul_assoc, inv_mul_self, mul_one, hσ, ← h₁,
-      ← linear_map.comp_apply, inner_aut_comp_inner_aut], },
-  { rintros ⟨U, hU⟩,
-    simp_rw [hU, ← linear_map.comp_apply, inner_aut_comp_inner_aut, inner_aut.spectrum_eq], },
+  { rcases hA₁.schur_decomp with ⟨D₁, U₁, h₁⟩,
+    rcases hA₂.schur_decomp with ⟨D₂, U₂, h₂⟩,
+    have hA₁' : is_almost_hermitian (inner_aut U₁ (diagonal D₁)) :=
+    by rw [h₁]; exact hA₁,
+    have hA₂' : is_almost_hermitian (inner_aut U₂ (diagonal D₂)) :=
+    by rw [h₂]; exact hA₂,
+    have h₁' : hA₁.spectra = hA₁'.spectra :=
+    by { simp_rw [h₁], },
+    have h₂' : hA₂.spectra = hA₂'.spectra :=
+    by { simp_rw [h₂], },
+    rw [h₁', h₂'],
+    simp_rw [is_almost_hermitian.inner_aut_spectra, is_diagonal.spectrum_eq_iff_rotation],
+    rcases hA₁ with ⟨α₁, N₁, hA₁⟩,
+    rcases hA₂ with ⟨α₂, N₂, hA₂⟩,
+    simp_rw [← h₁, ← h₂],
+    rw [inner_aut_eq_iff] at h₁ h₂,
+    rintros ⟨U, hU⟩,
+    simp_rw [hU, inner_aut_apply_inner_aut_inv, inner_aut_eq_iff,
+      inner_aut_apply_inner_aut, _root_.mul_inv_rev, inv_inv],
+    use U₁ * (⟨(equiv.to_pequiv U).to_matrix,
+      equiv.perm.to_pequiv.to_matrix_mem_unitary_group _⟩ : unitary_group n 𝕜) * U₂⁻¹,
+    simp_rw [_root_.mul_inv_rev, inv_inv, mul_assoc, inv_mul_self, mul_one,
+      inv_mul_cancel_left, mul_inv_self, inner_aut_one, linear_map.one_apply], },
+  { rintros ⟨U, rfl⟩,
+    simp_rw [is_almost_hermitian.inner_aut_spectra], },
 end
 
 /-- two matrices are _almost similar_ if there exists some
@@ -153,18 +140,10 @@ def is_almost_similar_to [fintype n] [decidable_eq n] [is_R_or_C 𝕜] (x y : ma
   `matrix.is_almost_similar_to` and `matrix.has_almost_equal_spectra_to` -/
 lemma is_almost_hermitian.has_almost_equal_spectra_to_iff_is_almost_similar_to
   [linear_order n] {x y : matrix n n ℂ} (hx : x.is_almost_hermitian) (hy : y.is_almost_hermitian) :
-  x.has_almost_equal_spectra_to y ↔ x.is_almost_similar_to y :=
+  hx.has_almost_equal_spectra_to hy ↔ x.is_almost_similar_to y :=
 begin
-  have : (∃ (β : ℂˣ), spectrum ℂ (to_lin' x) = spectrum ℂ (to_lin' ((β : ℂ) • y)))
-    ↔ (∃ β : ℂ, β ≠ 0 ∧ spectrum ℂ (to_lin' x) = spectrum ℂ (to_lin' (β • y))) :=
-  ⟨λ ⟨β, hβ⟩, ⟨(β : ℂ), ⟨units.ne_zero _, hβ⟩⟩, λ ⟨β, ⟨hβ, h⟩⟩, ⟨units.mk0 β hβ, h⟩⟩,
-  simp_rw [matrix.has_almost_equal_spectra_to, this, is_almost_hermitian.spectrum_eq_iff hx
-    (almost_hermitian_iff_smul.mp hy _), matrix.is_almost_similar_to],
-  split,
-  { rintros ⟨β, ⟨hβ, ⟨U, hU⟩⟩⟩,
-    exact ⟨units.mk0 β hβ, U, hU⟩, },
-  { rintros ⟨β, U, hU⟩,
-    exact ⟨β, ⟨units.ne_zero _, ⟨U, hU⟩⟩⟩, },
+  simp_rw [is_almost_hermitian.has_almost_equal_spectra_to,
+    is_almost_hermitian.spectrum_eq_iff, matrix.is_almost_similar_to],
 end
 
 
diff --git a/src/linear_algebra/kronecker_to_tensor.lean b/src/linear_algebra/kronecker_to_tensor.lean
index 2906183a69..4d7f0b3f6d 100644
--- a/src/linear_algebra/kronecker_to_tensor.lean
+++ b/src/linear_algebra/kronecker_to_tensor.lean
@@ -3,10 +3,6 @@ Copyright (c) 2023 Monica Omar. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Monica Omar
 -/
-import linear_algebra.contraction
-import ring_theory.matrix_algebra
-import data.matrix.kronecker
-import data.matrix.dmatrix
 import linear_algebra.my_matrix.basic
 import linear_algebra.tensor_finite
 
@@ -141,7 +137,7 @@ begin
     algebra.tensor_product.tmul_mul_tmul, matrix.mul_eq_mul],
 end
 
-def tensor_to_kronecker :
+@[simps] def tensor_to_kronecker :
   (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] (matrix (m × n) (m × n) R) :=
 { to_fun := tensor_product.to_kronecker,
   inv_fun := matrix.kronecker_to_tensor_product,
@@ -162,12 +158,12 @@ lemma kronecker_to_tensor_to_linear_map_eq :
       : matrix (n × m) (n × m) R →ₗ[R] matrix n n R ⊗[R] matrix m m R) :=
 rfl
 
-end
-
-lemma tensor_to_kronecker_to_linear_map_eq {R m n : Type*} [comm_semiring R]
-  [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :
-  (tensor_to_kronecker
-    : (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] matrix (m × n) (m × n) R).to_linear_map
+lemma tensor_to_kronecker_to_linear_map_eq :
+  (((@tensor_to_kronecker R m n _ _ _ _ _
+    : (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] _).to_linear_map)
+    : (matrix m m R ⊗[R] matrix n n R) →ₗ[R] matrix (m × n) (m × n) R)
   = (tensor_product.to_kronecker
     : (matrix m m R ⊗[R] matrix n n R) →ₗ[R] matrix (m × n) (m × n) R) :=
 rfl
+
+end
\ No newline at end of file
diff --git a/src/linear_algebra/my_matrix/basic.lean b/src/linear_algebra/my_matrix/basic.lean
index 9dcec91ff3..84a1df79f3 100644
--- a/src/linear_algebra/my_matrix/basic.lean
+++ b/src/linear_algebra/my_matrix/basic.lean
@@ -295,7 +295,7 @@ open_locale matrix
 variables {R n m : Type*} [semiring R] [star_add_monoid R]
   [decidable_eq n] [decidable_eq m]
 
-@[simp] lemma matrix.std_basis_matrix_conj_transpose (i : n) (j : m) (a : R) :
+lemma matrix.std_basis_matrix_conj_transpose (i : n) (j : m) (a : R) :
   (matrix.std_basis_matrix i j a)ᴴ = matrix.std_basis_matrix j i (star a) :=
 begin
   simp_rw [matrix.std_basis_matrix, ite_and],
@@ -315,19 +315,19 @@ begin
     exact h H, },
 end
 
-@[simp] lemma matrix.std_basis_matrix.star_apply (i k : n) (j l : m) (a : R) :
+lemma matrix.std_basis_matrix.star_apply (i k : n) (j l : m) (a : R) :
   star (matrix.std_basis_matrix i j a k l) = matrix.std_basis_matrix j i (star a) l k :=
 begin
   rw [← matrix.std_basis_matrix_conj_transpose, ← matrix.conj_transpose_apply],
 end
 
-@[simp] lemma matrix.std_basis_matrix.star_apply' (i : n) (j : m) (x : n × m) (a : R) :
+lemma matrix.std_basis_matrix.star_apply' (i : n) (j : m) (x : n × m) (a : R) :
   star (matrix.std_basis_matrix i j a x.fst x.snd)
     = matrix.std_basis_matrix j i (star a) x.snd x.fst :=
 by rw matrix.std_basis_matrix.star_apply
 
 /-- $e_{ij}^*=e_{ji}$ -/
-@[simp] lemma matrix.std_basis_matrix.star_one {R : Type*} [semiring R]
+lemma matrix.std_basis_matrix.star_one {R : Type*} [semiring R]
   [star_ring R] (i : n) (j : m) :
   (matrix.std_basis_matrix i j (1 : R))ᴴ = matrix.std_basis_matrix j i (1 : R) :=
 begin
@@ -336,11 +336,11 @@ begin
 end
 
 open_locale big_operators
-@[simp] lemma matrix.trace_iff {R n : Type*} [add_comm_monoid R] [fintype n] (x : matrix n n R) :
+lemma matrix.trace_iff {R n : Type*} [add_comm_monoid R] [fintype n] (x : matrix n n R) :
   x.trace = ∑ k : n, (x k k) :=
 rfl
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply_basis {R p q : Type*} [semiring R]
+lemma matrix.std_basis_matrix.mul_apply_basis {R p q : Type*} [semiring R]
   [decidable_eq p] [decidable_eq q] (i x : n) (j y : m) (k z : p) (l w : q) :
   matrix.std_basis_matrix k l (matrix.std_basis_matrix i j (1 : R) x y) z w
     = (matrix.std_basis_matrix i j (1 : R) x y) * (matrix.std_basis_matrix k l (1 : R) z w) :=
@@ -349,7 +349,7 @@ begin
     and_rotate, and_assoc, and_comm],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply_basis' {R p q : Type*} [semiring R]
+lemma matrix.std_basis_matrix.mul_apply_basis' {R p q : Type*} [semiring R]
   [decidable_eq p] [decidable_eq q] (i x : n) (j y : m) (k z : p) (l w : q) :
   matrix.std_basis_matrix k l (matrix.std_basis_matrix i j (1 : R) x y) z w
     = ite (i = x ∧ j = y ∧ k = z ∧ l = w) 1 0 :=
@@ -358,7 +358,7 @@ begin
            zero_mul, one_mul],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply {R : Type*} [fintype n] [semiring R]
+lemma matrix.std_basis_matrix.mul_apply {R : Type*} [fintype n] [semiring R]
   (i j k l m p : n) :
   ∑ (x x_1 : n × n) (x_2 x_3 : n),
     matrix.std_basis_matrix l k (matrix.std_basis_matrix p m (1 : R) x_1.snd x_1.fst) x.snd x.fst
@@ -391,7 +391,7 @@ begin
   refl,
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_std_basis_matrix
+lemma matrix.std_basis_matrix.mul_std_basis_matrix
   {R p : Type*} [semiring R] [decidable_eq p] [fintype m]
   (i x : n) (j k : m) (l y : p) (a b : R) :
   ((matrix.std_basis_matrix i j a) ⬝ (matrix.std_basis_matrix k l b)) x y =
@@ -402,7 +402,7 @@ begin
     finset.sum_const_zero, eq_comm],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_std_basis_matrix' {R p : Type*}
+lemma matrix.std_basis_matrix.mul_std_basis_matrix' {R p : Type*}
   [fintype n] [decidable_eq p] [semiring R]
   (i : m) (j k : n) (l : p) :
   matrix.std_basis_matrix i j (1 : R) ⬝ matrix.std_basis_matrix k l (1 : R)
diff --git a/src/linear_algebra/my_matrix/is_almost_hermitian.lean b/src/linear_algebra/my_matrix/is_almost_hermitian.lean
index 17e25487e2..3dce1e9b9f 100644
--- a/src/linear_algebra/my_matrix/is_almost_hermitian.lean
+++ b/src/linear_algebra/my_matrix/is_almost_hermitian.lean
@@ -213,10 +213,4 @@ begin
   exact ⟨rfl, hx⟩,
 end
 
-/-- we say a matrix $x$ _has almost equal spectra to_ another matrix $y$ if
-  there exists some scalar $0\neq\beta \in \mathbb{C}$ such that $x$ and $\beta y$ have equal spectra -/
-def has_almost_equal_spectra_to [fintype n] [decidable_eq n] [field 𝕜]
-  (x y : matrix n n 𝕜) : Prop :=
-∃ β : 𝕜ˣ, spectrum 𝕜 x.to_lin' = spectrum 𝕜 ((β : 𝕜) • y).to_lin'
-
 end matrix
diff --git a/src/linear_algebra/my_matrix/spectra.lean b/src/linear_algebra/my_matrix/spectra.lean
index 6e8fc8a80e..8729e9e920 100644
--- a/src/linear_algebra/my_matrix/spectra.lean
+++ b/src/linear_algebra/my_matrix/spectra.lean
@@ -1,4 +1,21 @@
 import linear_algebra.my_matrix.basic
+import linear_algebra.inner_aut
+
+
+instance multiset_coe {α β : Type*} [has_coe α β] :
+  has_coe (multiset α) (multiset β) :=
+{ coe := λ s, s.map (coe : α → β) }
+lemma finset.val.map_coe {α β γ : Type*}
+  (f : α → β) (s : finset α) [has_coe β γ] :
+  ((s.val.map f : multiset β) : multiset γ) = s.val.map ↑f :=
+begin
+  unfold_coes,
+  simp only [multiset.map_map, function.comp_app, add_monoid_hom.to_fun_eq_coe],
+end
+
+noncomputable instance multiset_coe_R_to_is_R_or_C {𝕜 : Type*} [is_R_or_C 𝕜] :
+  has_coe (multiset ℝ) (multiset 𝕜) :=
+@multiset_coe ℝ 𝕜 ⟨coe⟩
 
 namespace matrix
 
@@ -6,7 +23,120 @@ variables {n 𝕜 : Type*} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decida
 
 open_locale matrix
 
+noncomputable def is_almost_hermitian.scalar {n : Type*}
+  {x : matrix n n 𝕜} (hx : x.is_almost_hermitian) :
+  𝕜 :=
+by choose α hα using hx; exact α
+noncomputable def is_almost_hermitian.matrix {n : Type*}
+  {x : matrix n n 𝕜} (hx : x.is_almost_hermitian) :
+  matrix n n 𝕜 :=
+by choose y hy using (is_almost_hermitian.scalar._proof_1 hx); exact y
+lemma is_almost_hermitian.eq_smul_matrix
+  {n : Type*} {x : matrix n n 𝕜} (hx : x.is_almost_hermitian) :
+  x = hx.scalar • hx.matrix :=
+(is_almost_hermitian.matrix._proof_1 hx).1.symm
+lemma is_almost_hermitian.matrix_is_hermitian
+  {n : Type*} {x : matrix n n 𝕜} (hx : x.is_almost_hermitian) :
+  hx.matrix.is_hermitian :=
+(is_almost_hermitian.matrix._proof_1 hx).2
+
+noncomputable def is_almost_hermitian.eigenvalues {x : matrix n n 𝕜}
+  (hx : x.is_almost_hermitian) :
+  n → 𝕜 :=
+begin
+  intros i,
+  exact hx.scalar • hx.matrix_is_hermitian.eigenvalues i,
+end
+
+noncomputable def is_almost_hermitian.spectra {A : matrix n n 𝕜} (hA : A.is_almost_hermitian) : multiset 𝕜 :=
+finset.univ.val.map (λ i, hA.eigenvalues i)
+
 noncomputable def is_hermitian.spectra {A : matrix n n 𝕜} (hA : A.is_hermitian) : multiset ℝ :=
 finset.univ.val.map (λ i, hA.eigenvalues i)
 
+lemma is_hermitian.spectra_coe {A : matrix n n 𝕜} (hA : A.is_hermitian) :
+  (hA.spectra : multiset 𝕜) = finset.univ.val.map (λ i, hA.eigenvalues i) :=
+begin
+  unfold_coes,
+  simp only [multiset.map_map, is_hermitian.spectra],
+end
+
+open_locale big_operators
+lemma is_hermitian.mem_coe_spectra_diagonal {A : n → 𝕜} (hA : (diagonal A).is_hermitian)
+  (x : 𝕜) :
+  x ∈ (hA.spectra : multiset 𝕜) ↔ ∃ (i : n), A i = x :=
+begin
+  simp_rw [is_hermitian.spectra_coe, multiset.mem_map],
+  simp only [finset.mem_univ_val, true_and],
+  have : ((x : 𝕜) ∈ {b : 𝕜 | ∃ a, ↑(hA.eigenvalues a) = b}
+    ↔ (x : 𝕜) ∈ {b : 𝕜 | ∃ a, A a = b})
+    ↔
+    ((∃ a, (hA.eigenvalues a : 𝕜) = x) ↔ (∃ a, A a = x)),
+  { simp_rw [set.mem_set_of], },
+  rw ← this,
+  clear this,
+  revert x,
+  rw [← set.ext_iff, ← is_hermitian.spectrum, diagonal.spectrum],
+end
+lemma is_hermitian.spectra_set_eq_spectrum
+  {A : matrix n n 𝕜} (hA : A.is_hermitian) :
+  {x : 𝕜 | x ∈ (hA.spectra : multiset 𝕜)}
+    = spectrum 𝕜 (to_lin' A) :=
+begin
+  ext,
+  simp_rw [is_hermitian.spectra_coe, hA.spectrum, set.mem_set_of,
+    multiset.mem_map, finset.mem_univ_val, true_and],
+end
+
+lemma is_hermitian.of_inner_aut {A : matrix n n 𝕜} (hA : A.is_hermitian)
+  (U : unitary_group n 𝕜) :
+  (inner_aut U A).is_hermitian :=
+(is_hermitian.inner_aut_iff U A).mp hA
+
+lemma is_almost_hermitian_iff_smul {A : matrix n n 𝕜} :
+  A.is_almost_hermitian ↔ ∀ α : 𝕜, (α • A).is_almost_hermitian :=
+begin
+  split,
+  { rintros ⟨β, y, rfl, hy⟩ α,
+    rw [smul_smul],
+    exact ⟨α * β, y, rfl, hy⟩, },
+  { intros h,
+    specialize h 1,
+    rw one_smul at h,
+    exact h, },
+end
+
+lemma is_almost_hermitian.smul {A : matrix n n 𝕜} (hA : A.is_almost_hermitian) (α : 𝕜) :
+  (α • A).is_almost_hermitian :=
+is_almost_hermitian_iff_smul.mp hA _
+
+lemma is_almost_hermitian.of_inner_aut {A : matrix n n 𝕜} (hA : A.is_almost_hermitian)
+  (U : unitary_group n 𝕜) :
+  (inner_aut U A).is_almost_hermitian :=
+begin
+  obtain ⟨α, y, rfl, hy⟩ := hA,
+  refine ⟨α, inner_aut U y, _, hy.of_inner_aut _⟩,
+  simp_rw [smul_hom_class.map_smul],
+end
+
+lemma is_almost_hermitian_iff_of_inner_aut {A : matrix n n 𝕜} (U : unitary_group n 𝕜) :
+  A.is_almost_hermitian ↔ (inner_aut U A).is_almost_hermitian :=
+begin
+  refine ⟨λ h, h.of_inner_aut _, _⟩,
+  rintros ⟨α, y, h, hy⟩,
+  rw [eq_comm, inner_aut_eq_iff] at h,
+  rw [h, smul_hom_class.map_smul],
+  clear h,
+  revert α,
+  rw [← is_almost_hermitian_iff_smul],
+  apply is_almost_hermitian.of_inner_aut,
+  exact hy.is_almost_hermitian,
+end
+
+/-- we say a matrix $x$ _has almost equal spectra to_ another matrix $y$ if
+  there exists some scalar $0\neq\beta \in \mathbb{C}$ such that $x$ and $\beta y$ have equal spectra -/
+def is_almost_hermitian.has_almost_equal_spectra_to
+  {x y : matrix n n 𝕜} (hx : x.is_almost_hermitian) (hy : y.is_almost_hermitian) : Prop :=
+∃ β : 𝕜ˣ, hx.spectra = (hy.smul β).spectra
+
 end matrix
diff --git a/src/preq/equiv.lean b/src/preq/equiv.lean
new file mode 100644
index 0000000000..85968922ab
--- /dev/null
+++ b/src/preq/equiv.lean
@@ -0,0 +1,15 @@
+import linear_algebra.my_matrix.basic
+
+lemma equiv.perm.to_pequiv.to_matrix_mem_unitary_group {n : Type*} [decidable_eq n]
+  [fintype n] {𝕜 : Type*} [comm_ring 𝕜] [star_ring 𝕜] (σ : equiv.perm n) :
+  (equiv.to_pequiv σ).to_matrix ∈ matrix.unitary_group n 𝕜 :=
+begin
+  simp_rw [matrix.mem_unitary_group_iff, ← matrix.ext_iff, matrix.mul_eq_mul,
+    matrix.mul_apply, pequiv.to_matrix_apply, boole_mul, equiv.to_pequiv_apply,
+    matrix.one_apply, option.mem_def, matrix.star_apply, pequiv.to_matrix_apply,
+    star_ite, star_one, star_zero, finset.sum_ite_eq,
+    finset.mem_univ, if_true],
+  intros i j,
+  simp_rw [equiv.to_pequiv_apply, option.mem_def, eq_comm, function.injective.eq_iff
+    (equiv.injective _)],
+end
\ No newline at end of file
diff --git a/src/quantum_graph/qam_A_example.lean b/src/quantum_graph/qam_A_example.lean
index 109c141235..8611d2581b 100644
--- a/src/quantum_graph/qam_A_example.lean
+++ b/src/quantum_graph/qam_A_example.lean
@@ -8,7 +8,7 @@ import quantum_graph.iso
 import linear_algebra.to_matrix_of_equiv
 import linear_algebra.my_ips.mat_ips
 import quantum_graph.qam_A
-import linear_algebra.blackbox
+import linear_algebra.my_matrix.spectra
 
 section
 
@@ -289,31 +289,6 @@ begin
     finset.sum_const_zero, finset.sum_ite_eq, finset.mem_univ, if_true],
 end
 
-noncomputable def matrix.is_almost_hermitian.scalar {n : Type*}
-  {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
-  ℂ :=
-by choose α hα using hx; exact α
-noncomputable def matrix.is_almost_hermitian.matrix {n : Type*}
-  {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
-  matrix n n ℂ :=
-by choose y hy using (matrix.is_almost_hermitian.scalar._proof_1 hx); exact y
-lemma matrix.is_almost_hermitian.eq_smul_matrix
-  {n : Type*} {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
-  x = hx.scalar • hx.matrix :=
-(matrix.is_almost_hermitian.matrix._proof_1 hx).1.symm
-lemma matrix.is_almost_hermitian.matrix_is_hermitian
-  {n : Type*} {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
-  hx.matrix.is_hermitian :=
-(matrix.is_almost_hermitian.matrix._proof_1 hx).2
-
-noncomputable def matrix.is_almost_hermitian.eigenvalues {x : matrix n n ℂ}
-  (hx : x.is_almost_hermitian) :
-  n → ℂ :=
-begin
-  intros i,
-  exact hx.scalar • hx.matrix_is_hermitian.eigenvalues i,
-end
-
 private lemma prod.eq' {α β : Type*} {p r : α} {q s : β} :
   (p,q) = (r,s) ↔ (p = r ∧ q = s) :=
 prod.eq_iff_fst_eq_snd_eq
@@ -364,7 +339,148 @@ begin
   exact h,
 end
 
-theorem qam_A'.fin_two_iso (x y : {x : matrix (fin 2) (fin 2) ℂ // x ≠ 0})
+lemma spectra_fin_two {x : matrix (fin 2) (fin 2) ℂ}
+  (hx : (x : matrix (fin 2) (fin 2) ℂ).is_almost_hermitian) :
+  hx.spectra = {(hx.eigenvalues 0 : ℂ), (hx.eigenvalues 1 : ℂ)} :=
+rfl
+lemma spectra_fin_two' {x : matrix (fin 2) (fin 2) ℂ}
+  (hx : (x : matrix (fin 2) (fin 2) ℂ).is_almost_hermitian) :
+  hx.spectra = [(hx.eigenvalues 0 : ℂ), (hx.eigenvalues 1 : ℂ)] :=
+rfl
+lemma spectra_fin_two'' {α : Type*} (a : fin 2 → α) :
+  multiset.map (a : (fin 2) → α) finset.univ.val = {a 0, a 1} :=
+rfl
+lemma list.coe_inj {α : Type*} (l₁ l₂ : list α) :
+  (l₁ : multiset α) = l₂ ↔ l₁ ~ l₂ :=
+multiset.coe_eq_coe
+lemma spectra_fin_two_ext_aux {A : Type*} (α β γ : A) :
+  ({α, α} : multiset A) = {β, γ} ↔ α = β ∧ α = γ :=
+begin
+  simp only [multiset.insert_eq_cons],
+  split,
+  { intro h,
+    simp_rw [multiset.cons_eq_cons, multiset.singleton_inj, multiset.singleton_eq_cons_iff] at h,
+    rcases h with (h1 | ⟨h, cs, ⟨hcs₁, hcs₂⟩, ⟨hcs₃, hcs₄⟩⟩),
+    { exact h1, },
+    { exact ⟨hcs₁, hcs₃.symm⟩, }, },
+  { rintro ⟨rfl, rfl⟩,
+    refl, },
+end
+lemma spectra_fin_two_ext {α : Type*} (α₁ α₂ β₁ β₂ : α) :
+  ({α₁, α₂} : multiset α) = {β₁, β₂} ↔
+  ((α₁ = β₁ ∧ α₂ = β₂) ∨ (α₁ = β₂ ∧ α₂ = β₁)) :=
+begin
+  by_cases H₁ : α₁ = α₂,
+  { rw [H₁, spectra_fin_two_ext_aux],
+    split,
+    { rintros ⟨h1, h2⟩,
+      left,
+      exact ⟨h1, h2⟩, },
+    { rintros (⟨h1, h2⟩ | ⟨h1, h2⟩),
+      { exact ⟨h1, h2⟩, },
+      { exact ⟨h2, h1⟩, }, }, },
+  by_cases h' : α₁ = β₁,
+  { simp_rw [h', eq_self_iff_true, true_and, multiset.insert_eq_cons,
+      multiset.cons_inj_right, multiset.singleton_inj],
+    split,
+    { intro hi,
+      left,
+      exact hi, },
+    rintros (h | ⟨h1, h2⟩),
+    { exact h, },
+    { rw [← h', eq_comm] at h2,
+      contradiction, }, },
+  simp_rw [multiset.insert_eq_cons, multiset.cons_eq_cons,
+    multiset.singleton_inj, multiset.singleton_eq_cons_iff, ne.def, h', false_and, false_or,
+    not_false_iff, true_and],
+  simp only [exists_eq_right_right, eq_self_iff_true, and_true, and.congr_right_iff,
+    eq_comm, iff_self],
+  simp_rw [and_comm, iff_self],
+end
+@[instance] def multiset.has_smul {α : Type*} [has_smul ℂ α] :
+  has_smul ℂ (multiset α) :=
+{ smul := λ a s, s.map ((•) a), }
+lemma multiset.smul_fin_two {α : Type*} [has_smul ℂ α] (a b : α) (c : ℂ) :
+  (c • ({a, b} : multiset α) : multiset α) = {c • a, c • b} :=
+rfl
+lemma is_almost_hermitian.smul_eq {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) (c : ℂ) :
+  (hx.smul c).scalar • (hx.smul c).matrix = c • x := by
+{ rw [← (hx.smul c).eq_smul_matrix], }
+
+lemma spectra_fin_two_ext_of_traceless {α₁ α₂ β₁ β₂ : ℂ} (hα₂ : α₂ ≠ 0) (hβ₂ : β₂ ≠ 0)
+  (h₁ : α₁ = - α₂) (h₂ : β₁ = - β₂) :
+  ∃ c : ℂˣ, ({α₁, α₂} : multiset ℂ) = (c : ℂ) • {β₁, β₂} :=
+begin
+  simp_rw [h₁, h₂, multiset.smul_fin_two, smul_neg],
+  refine ⟨units.mk0 (α₂ * β₂⁻¹) (mul_ne_zero hα₂ (inv_ne_zero hβ₂)), _⟩,
+  simp_rw [units.coe_mk0, smul_eq_mul, mul_assoc, inv_mul_cancel hβ₂, mul_one],
+end
+lemma matrix.is_almost_hermitian.trace {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  x.trace = ∑ i, hx.eigenvalues i :=
+begin
+  simp_rw [is_almost_hermitian.eigenvalues, ← finset.smul_sum, ← is_hermitian.trace_eq,
+    ← trace_smul],
+  rw ← is_almost_hermitian.eq_smul_matrix hx,
+end
+noncomputable def matrix.is_almost_hermitian.eigenvector_matrix {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  matrix n n ℂ :=
+hx.matrix_is_hermitian.eigenvector_matrix
+lemma matrix.is_almost_hermitian.eigenvector_matrix_eq {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  hx.eigenvector_matrix = hx.matrix_is_hermitian.eigenvector_matrix :=
+rfl
+lemma matrix.is_almost_hermitian.eigenvector_matrix_mem_unitary_group {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  hx.eigenvector_matrix ∈ unitary_group n ℂ :=
+hx.matrix_is_hermitian.eigenvector_matrix_mem_unitary_group
+lemma matrix.is_almost_hermitian.spectral_theorem' {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  x = hx.scalar •
+  (inner_aut ⟨hx.matrix_is_hermitian.eigenvector_matrix, is_hermitian.eigenvector_matrix_mem_unitary_group _⟩
+    (diagonal (coe ∘ hx.matrix_is_hermitian.eigenvalues))) :=
+begin
+  rw [← is_hermitian.spectral_theorem', ← hx.eq_smul_matrix],
+end
+lemma matrix.is_almost_hermitian.eigenvalues_eq {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  hx.eigenvalues = hx.scalar • (coe ∘ hx.matrix_is_hermitian.eigenvalues : n → ℂ) :=
+rfl
+lemma matrix.is_almost_hermitian.spectral_theorem {x : matrix n n ℂ}
+  (hx : x.is_almost_hermitian) :
+  x = inner_aut ⟨hx.eigenvector_matrix, hx.eigenvector_matrix_mem_unitary_group⟩
+    (diagonal hx.eigenvalues) :=
+begin
+  simp_rw [hx.eigenvalues_eq, diagonal_smul, smul_hom_class.map_smul, hx.eigenvector_matrix_eq],
+  exact matrix.is_almost_hermitian.spectral_theorem' _,
+end
+lemma matrix.is_almost_hermitian.eigenvalues_eq_zero_iff
+  {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
+  hx.eigenvalues = 0 ↔ x = 0 :=
+begin
+  simp_rw [matrix.is_almost_hermitian.eigenvalues_eq, smul_eq_zero,
+    matrix.is_hermitian.eigenvalues_eq_zero_iff, ← smul_eq_zero],
+  rw [← hx.eq_smul_matrix],
+  simp only [iff_self],
+end
+private lemma matrix.is_almost_hermitian.eigenvalues_eq_zero_iff_aux
+  {x : matrix (fin 2) (fin 2) ℂ} (hx : x.is_almost_hermitian) :
+  hx.eigenvalues 0 = 0 ∧ hx.eigenvalues 1 = 0 ↔ x = 0 :=
+begin
+  rw [← hx.eigenvalues_eq_zero_iff, function.funext_iff],
+  simp_rw [fin.forall_fin_two, pi.zero_apply, iff_self],
+end
+
+lemma matrix.diagonal_eq_zero_iff {x : n → ℂ} :
+  diagonal x = 0 ↔ x = 0 :=
+begin
+  simp_rw [← diagonal_zero, diagonal_eq_diagonal_iff, function.funext_iff,
+    pi.zero_apply, iff_self],
+end
+
+theorem qam_A.fin_two_iso (x y : {x : matrix (fin 2) (fin 2) ℂ // x ≠ 0})
   (hx1 : _root_.is_self_adjoint (qam_A trace_is_faithful_pos_map.elim x))
   (hx2 : qam.refl_idempotent trace_is_faithful_pos_map.elim (qam_A trace_is_faithful_pos_map.elim x) 1 = 0)
   (hy1 : _root_.is_self_adjoint (qam_A trace_is_faithful_pos_map.elim y))
@@ -375,49 +491,69 @@ theorem qam_A'.fin_two_iso (x y : {x : matrix (fin 2) (fin 2) ℂ // x ≠ 0})
 begin
   simp_rw [qam_A.iso_iff, trace_module_dual_matrix, commute.one_left,
     and_true, smul_hom_class.map_smul],
-  have : is_almost_similar_to (x : matrix (fin 2) (fin 2) ℂ) (y : matrix (fin 2) (fin 2) ℂ)
-    ↔ ∃ (β : ℂˣ) (U : unitary_group (fin 2) ℂ), (x : matrix (fin 2) (fin 2) ℂ)
-      = (β : ℂ) • inner_aut U y :=
-  by simp_rw [is_almost_similar_to, ← inner_aut_eq_iff, smul_hom_class.map_smul,
-    eq_comm, iff_self],
   rw exists_comm,
   obtain ⟨Hx, hxq⟩ := (qam_A.is_self_adjoint_iff x).mp hx1,
   obtain ⟨Hy, hyq⟩ := (qam_A.is_self_adjoint_iff y).mp hy1,
-  simp_rw [← this, ← Hx.has_almost_equal_spectra_to_iff_is_almost_similar_to Hy,
-    has_almost_equal_spectra_to],
-  rw [Hx.eq_smul_matrix, Hy.eq_smul_matrix, Hx.matrix_is_hermitian.spectral_theorem',
-    Hy.matrix_is_hermitian.spectral_theorem'],
-  simp_rw [smul_smul, ← smul_hom_class.map_smul, inner_aut.spectrum_eq, ← diagonal_smul,
-    diagonal.spectrum, pi.smul_apply, function.comp_apply],
-  have hα : Hx.scalar ≠ 0,
-  { have := Hx.eq_smul_matrix,
-    intros i,
-    simp_rw [i, zero_smul, set.mem_set_of.mp (subtype.mem x)] at this,
-    exact this, },
-  have hβ : Hy.scalar ≠ 0,
-  { have := Hy.eq_smul_matrix,
-    intros i,
-    simp_rw [i, zero_smul, set.mem_set_of.mp (subtype.mem y)] at this,
-    exact this, },
-  have := hx2,
-  have this' := hy2,
-  rw [qam_A.is_irreflexive_iff] at this this',
-  rw [Hx.eq_smul_matrix, Hx.matrix_is_hermitian.spectral_theorem'] at this,
-  rw [Hy.eq_smul_matrix, Hy.matrix_is_hermitian.spectral_theorem'] at this',
-  rw [trace_smul, inner_aut_apply_trace_eq, smul_eq_zero] at this this',
-  simp_rw [trace_fin_two, diagonal_apply_eq, function.comp_apply, hα, hβ, false_or,
-    add_eq_zero_iff_eq_neg] at this this',
-  simp only [set.ext_iff, set.mem_set_of, fin.exists_fin_two],
-  simp_rw [this, this', smul_eq_mul, mul_neg],
-  have Hhx := example_aux Hx this 1,
-  have Hhy := example_aux Hy this' 1,
-  let eig₁ := units.mk0 _ Hhx,
-  let eig₂ := units.mk0 _ Hhy,
-  let s₁ := units.mk0 _ hα,
-  let s₂ := units.mk0 _ hβ,
-  use s₁ * eig₁ * eig₂⁻¹ * s₂⁻¹,
-  simp_rw [units.coe_mul, mul_assoc, eig₂, s₂, units.coe_inv, units.coe_mk0,
-    inv_mul_cancel_left₀ hβ, inv_mul_cancel Hhy, mul_one, iff_self, forall_true_iff],
+  simp_rw [qam_A.is_irreflexive_iff, Hx.trace, Hy.trace,
+    fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hx2 hy2,
+  rw [matrix.is_almost_hermitian.spectral_theorem Hx,
+    matrix.is_almost_hermitian.spectral_theorem Hy],
+  have HX : diagonal Hx.eigenvalues = of ![![-Hx.eigenvalues 1, 0], ![0, Hx.eigenvalues 1]],
+  { rw [← hx2, ← matrix.ext_iff],
+    simp only [fin.forall_fin_two, diagonal_apply, of_apply, eq_self_iff_true, if_true,
+      one_ne_zero, if_false, zero_ne_one, if_false],
+    simp only [cons_val_zero, eq_self_iff_true, cons_val_one, head_cons, and_self], },
+  have HY : diagonal Hy.eigenvalues = of ![![-Hy.eigenvalues 1, 0], ![0, Hy.eigenvalues 1]],
+  { rw [← hy2, ← matrix.ext_iff],
+    simp only [fin.forall_fin_two, diagonal_apply, of_apply, eq_self_iff_true, if_true,
+      one_ne_zero, if_false, zero_ne_one, if_false],
+    simp only [cons_val_zero, eq_self_iff_true, cons_val_one, head_cons, and_self], },
+  simp_rw [HY, HX, inner_aut_apply_inner_aut],
+  have hx₁ : Hx.eigenvalues 1 ≠ 0,
+  { intros hx₁,
+    have : diagonal Hx.eigenvalues = 0,
+    { rw [HX, hx₁, neg_zero, ← matrix.ext_iff],
+      simp_rw [fin.forall_fin_two],
+      simp only [of_apply, pi.zero_apply],
+      simp only [cons_val_zero, cons_val_one, head_cons, and_self], },
+    rw [matrix.diagonal_eq_zero_iff, matrix.is_almost_hermitian.eigenvalues_eq_zero_iff] at this,
+    exact (subtype.mem x) this, },
+  have hy₁ : Hy.eigenvalues 1 ≠ 0,
+  { intros hy₁,
+    have : diagonal Hy.eigenvalues = 0,
+    { rw [HY, hy₁, neg_zero, ← matrix.ext_iff],
+      simp_rw [fin.forall_fin_two],
+      simp only [of_apply, pi.zero_apply],
+      simp only [cons_val_zero, cons_val_one, head_cons, and_self], },
+    rw [matrix.diagonal_eq_zero_iff, matrix.is_almost_hermitian.eigenvalues_eq_zero_iff] at this,
+    exact (subtype.mem y) this, },
+  refine ⟨units.mk0 ((Hx.eigenvalues 1) * (Hy.eigenvalues 1)⁻¹)
+    (mul_ne_zero hx₁ (inv_ne_zero hy₁)),
+    ⟨Hx.eigenvector_matrix, Hx.eigenvector_matrix_mem_unitary_group⟩
+      * ⟨Hy.eigenvector_matrix, Hy.eigenvector_matrix_mem_unitary_group⟩⁻¹, _⟩,
+  have : (Hx.eigenvalues 1 * (Hy.eigenvalues 1)⁻¹) • diagonal Hy.eigenvalues = diagonal Hx.eigenvalues,
+  { rw [HX, HY],
+    simp only [smul_of, smul_cons, algebra.id.smul_eq_mul, mul_neg, mul_zero,
+      smul_empty, embedding_like.apply_eq_iff_eq],
+    simp only [inv_mul_cancel_right₀ hy₁], },
+  simp_rw [inv_mul_cancel_right, units.coe_mk0, ← smul_hom_class.map_smul, ← HY, ← HX, this],
+end
+
+theorem qam.fin_two_iso_of_single_edge
+  {A B : matrix (fin 2) (fin 2) ℂ →ₗ[ℂ] matrix (fin 2) (fin 2) ℂ}
+  (hx0 : real_qam trace_is_faithful_pos_map.elim A)
+  (hy0 : real_qam trace_is_faithful_pos_map.elim B)
+  (hx : hx0.edges = 1) (hy : hy0.edges = 1)
+  (hx1 : _root_.is_self_adjoint A)
+  (hx2 : qam.refl_idempotent trace_is_faithful_pos_map.elim A 1 = 0)
+  (hy1 : _root_.is_self_adjoint B)
+  (hy2 : qam.refl_idempotent trace_is_faithful_pos_map.elim B 1 = 0) :
+  @qam.iso (fin 2) _ _ (trace_module_dual) A B :=
+begin
+  rw [real_qam.edges_eq_one_iff] at hx hy,
+  obtain ⟨x, rfl⟩ := hx,
+  obtain ⟨y, rfl⟩ := hy,
+  exact qam_A.fin_two_iso x y hx1 hx2 hy1 hy2,
 end
 
 end