awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) then 1 else 0

Tactic:
simp [real_inner_eq_re_inner]

Premises used: real_inner_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) then 1 else 0

Tactic:
simp [real_inner_eq_re_inner]

Premises used: real_inner_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) then 1 else 0

Tactic:
simp [real_inner_eq_re_inner]

Premises used: real_inner_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
z : ℂ
⊢ ofLp (p := 2) ((orthonormalBasisOneI.repr : (a : ℂ) → EuclideanSpace ℝ (Fin 2)) z) = ![z.re, z.im]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
x : EuclideanSpace ℝ (Fin 2)
⊢ (orthonormalBasisOneI.repr.symm : (a : EuclideanSpace ℝ (Fin 2)) → ℂ) x = (↑(x.ofLp 0) : ℂ) + (↑(x.ofLp 1) : ℂ) * I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
⊢ orthonormalBasisOneI.toBasis = basisOneI

Tactic:
Basis.toBasis_toOrthonormalBasis _ _

Premises used: Module.Basis.toBasis_toOrthonormalBasis, Complex.orthonormalBasisOneI
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
⊢ (⇑orthonormalBasisOneI : (a : Fin 2) → ℂ) = ![1, I]

Tactic:
simp [Complex.orthonormalBasisOneI]

Premises used: Complex.orthonormalBasisOneI
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
F' : Type u_6
inst_2 : NormedAddCommGroup F'
inst_3 : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
simp :
  Eq (α := ℂ ≃ₗᵢ[ℝ] F') (orthonormalBasisOneI.repr.trans (v.repr.symm.trans f))
    (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
⊢ isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f

Tactic:
simp only [isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm]

Premises used: Complex.isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans, LinearIsometryEquiv.symm_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
F' : Type u_6
inst_2 : NormedAddCommGroup F'
inst_3 : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
rw rw₁ :
  Eq (α := ℂ ≃ₗᵢ[ℝ] F') (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
    (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
⊢ Eq (α := ℂ ≃ₗᵢ[ℝ] F') (orthonormalBasisOneI.repr.trans (v.repr.symm.trans f))
    (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)

Tactic:
rw [LinearIsometryEquiv.trans_assoc]

Premises used: LinearIsometryEquiv.trans_assoc
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
f : F
⊢ ((isometryOfOrthonormal v).symm : (a : F) → ℂ) f =
    (↑((v.toBasis.coord 0 : (a : F) → ℝ) f) : ℂ) + (↑((v.toBasis.coord 1 : (a : F) → ℝ) f) : ℂ) * I

Tactic:
simp [Complex.isometryOfOrthonormal]

Premises used: Complex.isometryOfOrthonormal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ (isometryOfOrthonormal v : (a : ℂ) → F) z =
    HSMul.hSMul (β := F) z.re ((v : (a : Fin 2) → F) 0 : F) + HSMul.hSMul (β := F) z.im ((v : (a : Fin 2) → F) 1 : F)

Tactic:
simp [Complex.isometryOfOrthonormal, ← v.sum_repr_symm]

Premises used: Complex.isometryOfOrthonormal, OrthonormalBasis.sum_repr_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
a₁ :
  ∀ (i j : ι),
    HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
        (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
      1 i j
⊢ (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ * a.toBasis.toMatrix (⇑b : (a : ι) → E) = 1

Tactic:
ext i j
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ inner 𝕜 (E := EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι') =
    inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)

Tactic:
a.repr.inner_map_map (b i) (b j)

Premises used: OrthonormalBasis.repr, LinearIsometryEquiv.inner_map_map, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
h :
  HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι')
h₁ : 1 i j = inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)
⊢ HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    1 i j

Tactic:
convert! a.repr.inner_map_map (b i) (b j)

Premises used: OrthonormalBasis.repr, LinearIsometryEquiv.inner_map_map, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
h :
  Eq.{u_3 + 1} (α := 𝕜)
    (∑ x : ι',
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E) x i) : 𝕜)
        (a.toBasis.toMatrix (⇑b : (a : ι) → E) x j))
    (∑ x : ι',
      HMul.hMul (α := 𝕜) (β := 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
            (ofLp (p := 2) ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) i)) x) :
          𝕜)
        (ofLp (p := 2) ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) j)) x : 𝕜))
⊢ HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    inner 𝕜 (E := EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) i) : EuclideanSpace 𝕜 ι')
      ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) j) : EuclideanSpace 𝕜 ι')

Tactic:
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, star_def, PiLp.inner_apply,
      inner_apply']

Premises used: RCLike.star_def, RCLike.inner_apply', Matrix.mul_apply, Matrix.conjTranspose_apply, PiLp.inner_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ Eq.{u_3 + 1} (α := 𝕜)
    (∑ x : ι',
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E) x i) : 𝕜)
        (a.toBasis.toMatrix (⇑b : (a : ι) → E) x j))
    (∑ x : ι',
      HMul.hMul (α := 𝕜) (β := 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
            (ofLp (p := 2) ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) i)) x) :
          𝕜)
        (ofLp (p := 2) ((a.repr : (a : E) → EuclideanSpace 𝕜 ι') ((b : (a : ι) → E) j)) x : 𝕜))

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
h : Eq.{u_3 + 1} (α := 𝕜) (1 i j) (if i = j then 1 else 0)
h₁ h₂ : Eq.{u_3 + 1} (α := 𝕜) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ 1 i j = inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)

Tactic:
rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]

Premises used: Matrix.one_apply, OrthonormalBasis.orthonormal, Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
rw : (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ * a.toBasis.toMatrix (⇑b : (a : ι') → E) = 1
rw₁ rw₂ : Eq (α := Matrix ι' ι' 𝕜) 1 1
⊢ a.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1

Tactic:
rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
    a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]

Premises used: Matrix.mul_eq_one_comm_of_equiv, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, Module.Basis.indexEquiv, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
rw : (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ * a.toBasis.toMatrix (⇑b : (a : ι') → E) = 1
rw₁ rw₂ : Eq (α := Matrix ι' ι' 𝕜) 1 1
⊢ a.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1

Tactic:
classical
  rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
    a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
rw :
  HMul.hMul (α := Matrix ι ι 𝕜) (star (a.toBasis.toMatrix (⇑b : (a : ι) → E))) (a.toBasis.toMatrix (⇑b : (a : ι) → E)) =
    1
⊢ Membership.mem (γ := Submonoid (Matrix ι ι 𝕜)) (Matrix.unitaryGroup ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))

Tactic:
rw [Matrix.mem_unitaryGroup_iff']

Premises used: Matrix.mem_unitaryGroup_iff'
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ HMul.hMul (α := Matrix ι ι 𝕜) (star (a.toBasis.toMatrix (⇑b : (a : ι) → E))) (a.toBasis.toMatrix (⇑b : (a : ι) → E)) =
    1

Tactic:
a.toMatrix_orthonormalBasis_conjTranspose_mul_self b

Premises used: OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ HMul.hMul (α := Matrix ι ι 𝕜) (star (a.toBasis.toMatrix (⇑b : (a : ι) → E))) (a.toBasis.toMatrix (⇑b : (a : ι) → E)) =
    1

Tactic:
exact a.toMatrix_orthonormalBasis_conjTranspose_mul_self b

Premises used: OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E)) * star (Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))) = 1

Tactic:
have := (Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)).2
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this :
  Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E)) * star (Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))) = 1
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ : 𝕜) 2 = 1

Tactic:
rw [star_def, RCLike.mul_conj] at this

Premises used: RCLike.star_def, RCLike.mul_conj
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ : 𝕜) 2 = 1
⊢ HPow.hPow (β := ℕ) ‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ 2 = 1

Tactic:
norm_cast at this
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : HPow.hPow (β := ℕ) ‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ 2 = 1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ = 1),
    Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1
⊢ Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1

Tactic:
rwa [pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at this

Premises used: two_ne_zero, pow_eq_one_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : Fintype ι
inst_3 : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ Membership.mem (γ := Submonoid (Matrix ι ι ℝ)) (Matrix.orthogonalGroup ι ℝ) (a.toBasis.toMatrix (⇑b : (a : ι) → F))

Tactic:
a.toMatrix_orthonormalBasis_mem_unitary b

Premises used: Set.Mem, setOf, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : Fintype ι
inst_3 : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
rw : HPow.hPow (α := ℝ) (β := ℕ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) 2 = 1
⊢ Eq (α := ℝ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) (1 : ℝ) ∨
    Eq (α := ℝ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) (-1 : ℝ)

Tactic:
rw [← sq_eq_one_iff]

Premises used: sq_eq_one_iff
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : Fintype ι
inst_3 : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) 2 = 1

Tactic:
simpa [unitary, sq] using Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)

Premises used: unitary, sq, Matrix.det_of_mem_unitary, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtypeₗᵢ
inst_8 : DecidableEq ι
hV_sum : IsInternal (S := Submodule 𝕜 E) fun (i : ι) ↦ A i
α : ι → Type u_7
inst_9 : (i : ι) → Fintype (α i)
v_family : (i : ι) → OrthonormalBasis.{u_7, u_3, u_4} (α i) 𝕜 ↥(A i)
⊢ ∀ (i : ι), Orthonormal.{u_3, u_4, u_7} 𝕜 (E := ↥(A i)) (ι := α i) (⇑(v_family i).toBasis : (a : α i) → ↥(A i))

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtypeₗᵢ
inst_8 : DecidableEq ι
hV_sum : IsInternal (S := Submodule 𝕜 E) fun (i : ι) ↦ A i
α : ι → Type u_7
inst_9 : (i : ι) → Fintype (α i)
v_family : (i : ι) → OrthonormalBasis.{u_7, u_3, u_4} (α i) 𝕜 ↥(A i)
⊢ Orthonormal 𝕜 (E := E) (ι := (i : ι) × α i)
    (⇑(hV_sum.collectedBasis (α := α) fun (i : ι) ↦ (v_family i).toBasis) : (a : (i : ι) × α i) → E)

Tactic:
simpa using
      hV.orthonormal_sigma_orthonormal (show ∀ i, Orthonormal 𝕜 (v_family i).toBasis by simp)

Premises used: OrthogonalFamily.orthonormal_sigma_orthonormal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
A : ι → Submodule 𝕜 E
inst_4 : DecidableEq ι
h : IsInternal A
α : ι → Type u_7
inst_5 : (i : ι) → Fintype (α i)
hV : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtypeₗᵢ
v : (i : ι) → OrthonormalBasis.{u_7, u_3, u_4} (α i) 𝕜 ↥(A i)
a : (i : ι) × α i
⊢ Membership.mem (α := E) (A (a.fst (β := fun (i : ι) ↦ α i)))
    ((collectedOrthonormalBasis hV h (α := α) v : (a : (i : ι) × α i) → E) a : E)

Tactic:
simp [DirectSum.IsInternal.collectedOrthonormalBasis]

Premises used: DirectSum.IsInternal.collectedOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
obtain :
  ∀ (u₀ : Set E) (hu₀s : u₀ ⊇ v)
    (hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀)))
    (hu₀_max :
      ∀ u ⊇ u₀,
        Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = u₀),
    ∃ (u : Finset E) (b : OrthonormalBasis (↥u) 𝕜 E),
      v ⊆ (↑u : Set E) ∧ Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑b : (a : ↥u) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
⊢ ∃ (u : Finset E) (b : OrthonormalBasis (↥u) 𝕜 E),
    v ⊆ (↑u : Set E) ∧ Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑b : (a : ↥u) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
obtain ⟨u₀, hu₀s, hu₀, hu₀_max⟩ := exists_maximal_orthonormal hv

Premises used: exists_maximal_orthonormal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max :
  ∀ u ⊇ u₀,
    Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = u₀
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥

Tactic:
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hu₀] at hu₀_max

Premises used: maximal_orthonormal_iff_orthogonalComplement_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
⊢ u₀.Finite

Tactic:
have hu₀_finite : u₀.Finite := hu₀.linearIndependent.setFinite
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
⊢ Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
simpa using hu₀.comp _ fu.injective

Premises used: Orthonormal.comp, Equiv.injective
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
inst_3 : FiniteDimensional 𝕜 E
hv : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := { x : E // x ∈ u₀ }) (Subtype.val (p := fun (x : E) ↦ x ∈ u₀))
hu₀_max : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset (s := u₀)
fu : ↥u ≃ (↑u₀ : Type u_4) := hu₀_finite.subtypeEquivToFinset (s := u₀).symm
⊢ Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))

Tactic:
have hu : Orthonormal 𝕜 ((↑) : u → E) := by simpa using hu₀.comp _ fu.injective