awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
x : ⨁ (i : ι), ↥(V i)
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
zero :
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) 0) =
    ((0 : ⨁ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i
of :
  ∀ (j : ι) (x : ↥(V j)),
    ((V i).orthogonalProjection : (a : E) → ↥(V i))
        ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
          (((DirectSum.of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) :
                (a : ↥(V j)) → ⨁ (i : ι), ↥(V i))
              x :
            ⨁ (i : ι), ↥(V i))) =
      ((((DirectSum.of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) :
                (a : ↥(V j)) → ⨁ (i : ι), ↥(V i))
              x :
            ⨁ (i : ι), ↥(V i)) :
          (a : ι) → ↥(V a))
        i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
    (x : (a : ι) → ↥(V a)) i
have add : ∀ (x y : ⨁ (i : ι), ↥(V i))
  (hx :
    ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
      (x : (a : ι) → ↥(V a)) i)
  (hy :
    ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) y) =
      (y : (a : ι) → ↥(V a)) i),
  ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) (x + y)) =
    (x + y : (a : ι) → ↥(V a)) i
Tactic: induction x using DirectSum.induction_on with
  | zero => simp
  | of j x =>
    simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
      -- Need to unfold `DirectSum` to see through the defeq abuse.
      DirectSum, DFinsupp.singleAddHom_apply]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
    · rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
        DFinsupp.single_eq_of_ne hij]
      exact hV.isOrtho hij.symm x.prop
  | add x y hx hy =>
    simp_rw [map_add]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ (DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x
have rw : (DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (V i) :
      (a : ⨁ (i : ι), ↥(V i)) → E)
    ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
      fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
  x
Tactic: rw [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid, DFinsupp.liftAddHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ (DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (V i) :
        (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x
have erw : (DFinsupp.sum (β := fun (i : ι) ↦ ↥(V i))
    ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
      fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
    fun (x : ι) ↦ (⇑(AddSubmonoidClass.subtype (V x) : ↥(V x) →+ E) : (a : ↥(V x)) → E)) =
  x
Tactic: erw [DFinsupp.sumAddHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ ↥(V i))
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
      fun (x : ι) ↦ (⇑(AddSubmonoidClass.subtype (V x) : ↥(V x) →+ E) : (a : ↥(V x)) → E)) =
    x
have rw : ∑ i : ι,
    ((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E)
      ((DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i)) : (a : Π₀ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
          ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
              (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
            fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
          i :
        ↥(V i)) =
  x
Tactic: rw [DFinsupp.sum_eq_sum_fintype]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
rw :
  ∑ i : ι,
      ((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E)
        ((DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i)) : (a : Π₀ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
                (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
              fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
            i :
          ↥(V i)) =
    x
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ ↥(V i))
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
      fun (x : ι) ↦ (⇑(AddSubmonoidClass.subtype (V x) : ↥(V x) →+ E) : (a : ↥(V x)) → E)) =
    x
have hf : ∀ (i : ι), Eq (α := E) (((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E) 0 : E) (0 : E)
Tactic: rw [DFinsupp.sum_eq_sum_fintype]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
⊢ ∑ i : ι,
      ((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E)
        ((DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i)) : (a : Π₀ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
                (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
              fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
            i :
          ↥(V i)) =
    x
have simp_rw : ∑ x_1 : ι, (↑(((V x_1).orthogonalProjection : (a : E) → ↥(V x_1)) x) : E) = x
Tactic: simp_rw [Equiv.apply_symm_apply, AddSubmonoidClass.coe_subtype]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : ⨁ (i : ι), ↥(V i)
⊢ ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
      fun (i : ι) ↦
      ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x)) =
    x
have simp_rw : ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) : (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
    fun (i : ι) ↦ (x : (a : ι) → ↥(V a)) i) =
  x
Tactic: simp_rw [hV.projection_directSum_coeAddHom, DFinsupp.equivFunOnFintype_symm_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) ↔
    Eq (α := Submodule 𝕜 E) (span 𝕜 v)ᗮ ⊥
have rw : (∀ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = v) ↔
  ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
Tactic: rw [Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) ↔
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
have mp : (∀ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = v) →
  ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
mp :
  (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) →
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
⊢ (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) ↔
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
have mpr : (∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0) →
  ∀ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = v
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
⊢ (∀ u ⊇ v,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
        u = v) →
    ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x → x = 0
have mp : (∃ (x : E), Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x ∧ x ≠ 0) →
  ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
⊢ ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
have he : ‖e‖ = 1
Tactic: have he : ‖e‖ = 1 := by simp [e, norm_smul_inv_norm hx]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
⊢ ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
have he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
Tactic: have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
hev : e ∈ v
⊢ e = 0
have this : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v ⊓ (span 𝕜 v)ᗮ) e
Tactic: have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
hev : e ∈ v
⊢ False
have this : e = 0
Tactic: have : e = 0 := by
        have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
hev : e ∈ v
this : e = 0
⊢ False
have this₁ : e ≠ 0
Tactic: have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
⊢ ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
have he'' : e ∉ v
Tactic: have he'' : e ∉ v := by
      intro hev
      have : e = 0 := by
        have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
      have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
      contradiction
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
⊢ ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
have mp : ∀ (i : { x : E // x ∈ insert e v }), ‖(↑i : E)‖ = 1
Tactic: refine ⟨insert e v, v.subset_insert e, ⟨?_, ?_⟩, (ne_insert_of_notMem v he'').symm⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
mp : ∀ (i : { x : E // x ∈ insert e v }), ‖(↑i : E)‖ = 1
⊢ ∃ u ⊇ v,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) ∧ u ≠ v
have mp₁ : Pairwise fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0
Tactic: refine ⟨insert e v, v.subset_insert e, ⟨?_, ?_⟩, (ne_insert_of_notMem v he'').symm⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
a : E
ha' : a ∈ insert e v
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
have mp : ∀ (ha : a = e), ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
Tactic: rcases eq_or_mem_of_mem_insert ha' with ha | ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
a : E
ha' : a ∈ insert e v
mp : ∀ (ha : a = e), ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
⊢ ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
have mp₁ : ∀ (ha : a ∈ v), ‖(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') : E)‖ = 1
Tactic: rcases eq_or_mem_of_mem_insert ha' with ha | ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
⊢ Pairwise fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0
have h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
Tactic: have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0 := by
        intro a ha
        exact he' a (Submodule.subset_span ha)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ v }) (Subtype.val (p := fun (x : E) ↦ x ∈ v))
x : E
hx' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ x
hx : x ≠ 0
e : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x
he : ‖e‖ = 1
he' : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 v)ᗮ e
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
⊢ ∀ ⦃j : { x : E // x ∈ insert e v }⦄,
    Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ j →
      (fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') j
have mp : ∀ (ha : a = e) ⦃j : { x : E // x ∈ insert e v }⦄,
  Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha' ≠ j →
    (fun (i j : { x : E // x ∈ insert e v }) ↦ ⟪(↑i : E), (↑j : E)⟫_𝕜 = 0)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ insert e v) a ha') j
Tactic: rcases eq_or_mem_of_mem_insert ha' with ha | ha