ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ star (Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) * Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b = 1
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b ∈ Matrix.unitaryGroup ι 𝕜
rw [Matrix.mem_unitaryGroup_iff']
case a.h
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ (star (Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) * Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) i j =
    OfNat.ofNat 1 i j
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ star (Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) * Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b = 1
ext (i j)
case h.e'_3
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ OfNat.ofNat 1 i j = inner (↑b i) (↑b j)
case a.h
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ (star (Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) * Basis.toMatrix (OrthonormalBasis.toBasis a) ↑b) i j =
    OfNat.ofNat 1 i j
convert a.repr.inner_map_map (b i) (b j)
case h.e'_3
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ OfNat.ofNat 1 i j = if i = j then 1 else 0
case h.e'_3
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ OfNat.ofNat 1 i j = inner (↑b i) (↑b j)
rw [orthonormal_iff_ite.mp b.orthonormal i j]
no goals
case h.e'_3
ι : Type u_1
ι' : Type ?u.1459554
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1459583
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1459601
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1459621
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ OfNat.ofNat 1 i j = if i = j then 1 else 0
rfl