awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
have right : gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
have right : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
have right : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Tactic: repeat' right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
⊢ Orthonormal.{u_1, u_2, u_3} 𝕜 (E := E) fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦
    gramSchmidtNormed 𝕜 f (↑i : ι)
have refine : Pairwise fun (i j : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦
  inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) i)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) j) =
    0
Tactic: refine ⟨fun i => gramSchmidtNormed_unit_length' i.prop, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
i j : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)
hij : ¬i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) i)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) j) =
    0
have hij₁ : ¬(↑i : ι) = (↑j : ι)
Tactic: rw [Subtype.ext_iff] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
s : Set ι
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' s)) (span 𝕜 (gramSchmidt 𝕜 f '' s))
have refine : ∀ (i : ι) (hi : i ∈ s),
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' (↑{i} : Set ι))) (gramSchmidt 𝕜 f i)
Tactic: refine span_eq_span
    (Set.image_subset_iff.2 fun i hi => smul_mem _ _ <| subset_span <| mem_image_of_mem _ hi)
    (Set.image_subset_iff.2 fun i hi =>
      span_mono (image_mono <| singleton_subset_set_iff.2 hi) ?_)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' (↑{i} : Set ι))) (gramSchmidt 𝕜 f i)
have simp : Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
Tactic: simp only [coe_singleton, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
have pos : ∀ (h : gramSchmidt 𝕜 f i = 0), Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
Tactic: by_cases h : gramSchmidt 𝕜 f i = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
pos :
  ∀ (h : gramSchmidt 𝕜 f i = 0), Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
have neg : ∀ (h : ¬gramSchmidt 𝕜 f i = 0), Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
Tactic: by_cases h : gramSchmidt 𝕜 f i = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
have neg : Ne.{u_1 + 1} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜) 0
Tactic: refine mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ ?_ _⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f)
have unfold : LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := E) fun (n : ι) ↦
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)
Tactic: unfold gramSchmidtNormed
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := E) fun (n : ι) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)
have this : ∀ (i : ι), IsUnit.{u_1} (M := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹
Tactic: have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) :=
    isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
⊢ gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f i) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
Tactic: rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
⊢ gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
Tactic: rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
⊢ (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
have H : gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
Tactic: have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by
    rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
⊢ (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
have rw : gramSchmidtNormed 𝕜 f i ≠ 0
Tactic: rw [gramSchmidtOrthonormalBasis_apply h, H]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) i, f j⟫_𝕜 = 0
have rw : Membership.mem (γ := Submodule 𝕜 E)
  (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)
Tactic: rw [← mem_orthogonal_singleton_iff_inner_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)
have a : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)) (f j)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)) (f j)
have a : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f j)
Tactic: rw [span_gramSchmidtNormed]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)
have suffices : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
  span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
Tactic: suffices span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ gramSchmidtOrthonormalBasis h f i by
    apply this
    rw [span_gramSchmidtNormed]
    exact mem_span_gramSchmidt 𝕜 f le_rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
have rw : ∀ ⦃u : E⦄,
  u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j →
    ∀ ⦃v : E⦄,
      Membership.mem (γ := Set E) (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)) v →
        ⟪u, v⟫_𝕜 = 0
Tactic: rw [isOrtho_span]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
have pos : ∀ (hk : gramSchmidtNormed 𝕜 f k = 0), ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
Tactic: by_cases hk : gramSchmidtNormed 𝕜 f k = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
pos :
  ∀ (hk : gramSchmidtNormed 𝕜 f k = 0),
    ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
have neg : ∀ (hk : ¬gramSchmidtNormed 𝕜 f k = 0),
  ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
Tactic: by_cases hk : gramSchmidtNormed 𝕜 f k = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : gramSchmidtNormed 𝕜 f k = 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
have pos : inner.{u_1, u_2} 𝕜 (E := E) (0 : E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) = 0
Tactic: rw [hk, inner_zero_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : gramSchmidtNormed 𝕜 f k = 0
pos : inner.{u_1, u_2} 𝕜 (E := E) (0 : E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) = 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
have pos₁ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [hk, inner_zero_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
have neg : inner.{u_1, u_2} 𝕜 (E := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) k : E)
    ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) =
  0
Tactic: rw [← gramSchmidtOrthonormalBasis_apply h hk]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) k : E)
      ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) =
    0
have this : k ≠ i
Tactic: have : k ≠ i := by
    rintro rfl
    exact hk hi
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
have pos : ∀ (hi : gramSchmidtNormed 𝕜 f j = 0), ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
Tactic: by_cases hi : gramSchmidtNormed 𝕜 f j = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
pos : ∀ (hi : gramSchmidtNormed 𝕜 f j = 0), ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
have neg : ∀ (hi : ¬gramSchmidtNormed 𝕜 f j = 0), ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
Tactic: by_cases hi : gramSchmidtNormed 𝕜 f j = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : gramSchmidtNormed 𝕜 f j = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
have pos : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_gramSchmidtOrthonormalBasis_eq_zero h hi]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst_8 : DecidableEq ι
⊢ Eq.{u_1 + 1} (α := 𝕜) (((gramSchmidtOrthonormalBasis h f).toBasis.det : (a : ι → E) → 𝕜) f : 𝕜)
    (∏ i : ι, ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) i, f i⟫_𝕜 : 𝕜)
have h₁ : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) x, f x⟫_𝕜 =
      (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x x
Tactic: convert! Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
⊢ HarmonicAt f₁ x ↔ HarmonicAt f₂ x
have mp : HarmonicAt f₁ x → HarmonicAt f₂ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
mp : HarmonicAt f₁ x → HarmonicAt f₂ x
⊢ HarmonicAt f₁ x ↔ HarmonicAt f₂ x
have mpr : HarmonicAt f₂ x → HarmonicAt f₁ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ ∀ᶠ (y : E) in 𝓝 x, HarmonicAt f y
have h₁ : ∀ (a : E) (h₁a : ContDiffAt ℝ 2 f a) (h₂a : ∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x), HarmonicAt f a
Tactic: filter_upwards [h.1.eventually (by simp), h.2.eventually_nhds] with a h₁a h₂a
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ + f₂) x
have left : ContDiffAt ℝ 2 (f₁ + f₂) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
left : ContDiffAt ℝ 2 (f₁ + f₂) x
⊢ HarmonicAt (f₁ + f₂) x
have right : Δ (f₁ + f₂) =ᶠ[𝓝 x] 0
Tactic: constructor