awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
j : Fin 2
0 :
  inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ) =
    if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) then 1 else 0
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ = j then 1 else 0
have 0₁ : inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℂ)
    ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℂ) =
  if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) then 1 else 0
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
j : Fin 2
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ = j then 1 else 0
have 1 : inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℂ)
    ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℂ) =
  if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) then 1 else 0
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 ι
j : Fin 2
1 :
  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
⊢ inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℂ)
      ((basisOneI : (a : Fin 2) → ℂ) j : ℂ) =
    if (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ = j then 1 else 0
have 1₁ : inner ℝ (E := ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℂ)
    ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℂ) =
  if Eq (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) then 1 else 0
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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'
⊢ isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f
have simp : Eq (α := ℂ ≃ₗᵢ[ℝ] F') (orthonormalBasisOneI.repr.trans (v.repr.symm.trans f))
  (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
Tactic: simp only [isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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'
⊢ Eq (α := ℂ ≃ₗᵢ[ℝ] F') (orthonormalBasisOneI.repr.trans (v.repr.symm.trans f))
    (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
have rw : Eq (α := ℂ ≃ₗᵢ[ℝ] F') (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
  (LinearIsometryEquiv.trans (orthonormalBasisOneI.repr.trans v.repr.symm) f)
Tactic: rw [LinearIsometryEquiv.trans_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ * a.toBasis.toMatrix (⇑b : (a : ι) → E) = 1
have a₁ : ∀ (i j : ι),
  HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    1 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 : ι
⊢ HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    1 i j
have 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 𝕜 ι')
Tactic: convert! a.repr.inner_map_map (b i) (b j)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 𝕜 ι')
⊢ HMul.hMul (α := Matrix ι ι' 𝕜) (β := Matrix ι' ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))ᴴ
      (a.toBasis.toMatrix (⇑b : (a : ι) → E)) i j =
    1 i j
have h₁ : 1 i j = inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)
Tactic: convert! a.repr.inner_map_map (b i) (b j)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 : ι
⊢ 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 𝕜 ι')
have 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 : 𝕜))
Tactic: simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, star_def, PiLp.inner_apply,
      inner_apply']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 : ι
⊢ 1 i j = inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)
have h : Eq.{u_3 + 1} (α := 𝕜) (1 i j) (if i = j then 1 else 0)
Tactic: rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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)
⊢ 1 i j = inner.{u_3, u_4} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((b : (a : ι) → E) j : E)
have h₁ : Eq.{u_3 + 1} (α := 𝕜) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1
have rw : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ a.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1
have rw₁ : Eq (α := Matrix ι' ι' 𝕜) 1 1
Tactic: rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
    a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1
have rw : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ a.toBasis.toMatrix (⇑b : (a : ι') → E) * (a.toBasis.toMatrix (⇑b : (a : ι') → E))ᴴ = 1
have rw₁ : Eq (α := Matrix ι' ι' 𝕜) 1 1
Tactic: classical
  rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
    a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ Membership.mem (γ := Submonoid (Matrix ι ι 𝕜)) (Matrix.unitaryGroup ι 𝕜) (a.toBasis.toMatrix (⇑b : (a : ι) → E))
have rw : HMul.hMul (α := Matrix ι ι 𝕜) (star (a.toBasis.toMatrix (⇑b : (a : ι) → E))) (a.toBasis.toMatrix (⇑b : (a : ι) → E)) = 1
Tactic: rw [Matrix.mem_unitaryGroup_iff']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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
⊢ Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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
⊢ Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1
have this₁ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ : 𝕜) 2 = 1
Tactic: rw [star_def, RCLike.mul_conj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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
⊢ Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1
have this₁ : HPow.hPow (β := ℕ) ‖Matrix.det (a.toBasis.toMatrix (⇑b : (a : ι) → E))‖ 2 = 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ Norm.norm.{u_3} (E := 𝕜) ((a.toBasis.det : (a : ι → E) → 𝕜) (⇑b : (a : ι) → E) : 𝕜) = 1
have 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
Tactic: rwa [pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
⊢ Eq (α := ℝ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) (1 : ℝ) ∨
    Eq (α := ℝ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) (-1 : ℝ)
have rw : HPow.hPow (α := ℝ) (β := ℕ) ((a.toBasis.det : (a : ι → F) → ℝ) (⇑b : (a : ι) → F) : ℝ) 2 = 1
Tactic: rw [← sq_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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 : 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))
have 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))
Tactic: obtain ⟨u₀, hu₀s, hu₀, hu₀_max⟩ := exists_maximal_orthonormal hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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₀
⊢ ∃ (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))
have hu₀_max₁ : Eq (α := Submodule 𝕜 E) (span 𝕜 u₀)ᗮ ⊥
Tactic: rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hu₀] at hu₀_max
Cleared hypotheses: hu₀_max
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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 : 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))
have hu₀_finite : u₀.Finite
Tactic: have hu₀_finite : u₀.Finite := hu₀.linearIndependent.setFinite
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
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
⊢ ∃ (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))
have hu : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (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))
have refine_1 : Eq.{u_4 + 1} (α := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))))ᗮ ⊥
Tactic: refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
refine_1 : Eq.{u_4 + 1} (α := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥u) (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))
have refine_2 : v ⊆ (↑u : Set E)
Tactic: refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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
hu : Orthonormal.{u_3, u_4, u_4} 𝕜 (E := E) (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))
refine_1 : Eq.{u_4 + 1} (α := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥u) (Subtype.val (p := fun (x : E) ↦ x ∈ u))))ᗮ ⊥
refine_2 : v ⊆ (↑u : Set E)
⊢ ∃ (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))
have refine_3 : Eq.{u_4 + 1} (α := (a : ↥u) → E) (⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu sorry) : (a : ↥u) → E)
  (Subtype.val (p := fun (x : E) ↦ x ∈ u))
Tactic: refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_7
inst_4 : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict («π» := fun (a : ι) ↦ E) v)
⊢ ∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, (b : (a : ι) → E) i = v i
have hsv : Injective (s.restrict («π» := fun (a : ι) ↦ E) v)
Tactic: have hsv : Injective (s.restrict v) := hv.linearIndependent.injective