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
n : ι
rw : gramSchmidt 𝕜 f n = f n - ∑ x ∈ (Iio n).attach, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
rw₁ : gramSchmidt 𝕜 f n = f n - ∑ x : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
⊢ gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
have rw₂ : f n - ∑ i : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑i : ι)) : (a : E) → E) (f n) =
  f n - ∑ x : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
Tactic: rw [← sum_attach, attach_eq_univ, gramSchmidt]
-- 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
n : ι
⊢ f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
have rw : f n =
  f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n) +
    ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
Tactic: rw [gramSchmidt_def, sub_add_cancel]
-- 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
n : ι
rw :
  f n =
    f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n) +
      ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
⊢ f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
have rw₁ : f n = f n
Tactic: rw [gramSchmidt_def, sub_add_cancel]
-- 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_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
have rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
Tactic: rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
-- 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_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
have rw₁ : f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
Tactic: rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
-- 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_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₁ : f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
have rw₂ : f ⊥ - ∑ i ∈ ∅, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
Tactic: rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
-- 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_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₁ : f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₂ : f ⊥ - ∑ i ∈ ∅, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
have rw₃ : f ⊥ - 0 = f ⊥
Tactic: rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
-- 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_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₁ : f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₂ : f ⊥ - ∑ i ∈ ∅, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₃ : f ⊥ - 0 = f ⊥
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
have rw₄ : f ⊥ = f ⊥
Tactic: rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
-- 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 ι
n : ι
⊢ Eq.{u_2 + 1} (α := E) (gramSchmidt 𝕜 0 n) 0
have rw : HSub.hSub (α := E) (0 n) (∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 0 i) : (a : E) → E) (0 n)) = 0
Tactic: rw [gramSchmidt_def]
-- 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have inl : ∀ (ha : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Tactic: rcases h₀.lt_or_gt with ha | hb
-- 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
inl : ∀ (ha : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have inr : ∀ (hb : b < a), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Tactic: rcases h₀.lt_or_gt with ha | hb
-- 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have inr : ⟪gramSchmidt 𝕜 f b, gramSchmidt 𝕜 f a⟫_𝕜 = 0
Tactic: rw [inner_eq_zero_symm]
-- 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
a b : ι
h₀ : a ≠ b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have suffices : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Tactic: suffices ∀ a b : ι, a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0 by
    rcases h₀.lt_or_gt with ha | hb
    · exact this _ _ ha
    · rw [inner_eq_zero_symm]
      exact this _ _ hb
-- 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
a b : ι
h₀ : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have revert : ∀ (a : ι) (h₀ : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Tactic: revert a
Cleared hypotheses: a, 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 ι
f : ι → E
b : ι
⊢ ∀ (a : ι) (h₀ : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have apply : ∀ (x : ι),
  (∀ y < x, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0) →
    ∀ (a : ι) (h₀ : a < x), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 = 0
Tactic: apply wellFounded_lt.induction b
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
have simp : ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
    ∑ x ∈ Iio b,
      ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 =
  0
Tactic: simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum,
    starProjection_singleton, inner_smul_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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ∑ x ∈ Iio b,
        ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 =
    0
have rw : ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
    ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
      ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
  0
Tactic: rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr 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 ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
rw :
  ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ∑ x ∈ Iio b,
        ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 =
    0
have rw₁ : ∀ b_2 ∈ Iio b,
  b_2 ≠ a →
    ⟪gramSchmidt 𝕜 f b_2, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f b_2‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b_2⟫_𝕜 =
      0
Tactic: rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr 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 ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
have pos : ∀ (h : gramSchmidt 𝕜 f a = 0),
  ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
Tactic: by_cases h : gramSchmidt 𝕜 f a = 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
pos :
  ∀ (h : gramSchmidt 𝕜 f a = 0),
    ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
        ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
      0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
have neg : ∀ (h : ¬gramSchmidt 𝕜 f a = 0),
  ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
Tactic: by_cases h : gramSchmidt 𝕜 f a = 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
have neg : ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0
Tactic: rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self]
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0
have neg : gramSchmidt 𝕜 f a ≠ 0
Tactic: rwa [inner_self_ne_zero]
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ ⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f i‖ 2) : 𝕜) *
      ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 =
    0
have simp : (⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 = 0 ∨ Eq.{u_1 + 1} (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f i‖ 2) : 𝕜) 0) ∨
  ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
Tactic: simp only [mul_eq_zero, div_eq_zero_iff]
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ (⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 = 0 ∨ Eq.{u_1 + 1} (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f i‖ 2) : 𝕜) 0) ∨
    ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
have h : ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
have h : ∀ (hia₁ : i < a), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
Tactic: rcases hia.lt_or_gt with hia₁ | hia₂
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
h : ∀ (hia₁ : i < a), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
have h₁ : ∀ (hia₂ : a < i), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
Tactic: rcases hia.lt_or_gt with hia₁ | hia₂
-- 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
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₁ : i < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
have h : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f a⟫_𝕜 = 0
Tactic: rw [inner_eq_zero_symm]
-- 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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j, v i⟫_𝕜 = 0
have rw : ⟪gramSchmidt 𝕜 v j,
    gramSchmidt 𝕜 v i +
      ∑ i_1 ∈ Iio i,
        (⟪gramSchmidt 𝕜 v i_1, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖gramSchmidt 𝕜 v i_1‖ : 𝕜) 2) •
          gramSchmidt 𝕜 v i_1⟫_𝕜 =
  0
Tactic: rw [gramSchmidt_def'' 𝕜 v]
-- 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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j,
      gramSchmidt 𝕜 v i +
        ∑ i_1 ∈ Iio i,
          (⟪gramSchmidt 𝕜 v i_1, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖gramSchmidt 𝕜 v i_1‖ : 𝕜) 2) •
            gramSchmidt 𝕜 v i_1⟫_𝕜 =
    0
have simp : ⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v i⟫_𝕜 +
    ∑ x ∈ Iio i,
      ⟪gramSchmidt 𝕜 v x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖gramSchmidt 𝕜 v x‖ : 𝕜) 2 *
        ⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v x⟫_𝕜 =
  0
Tactic: simp only [inner_add_right, inner_sum, inner_smul_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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ⟪b j, b i⟫_𝕜 + ∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0
have h : ⟪b j, b i⟫_𝕜 = 0
Tactic: convert! zero_add (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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
h : ⟪b j, b i⟫_𝕜 = 0
⊢ ⟪b j, b i⟫_𝕜 + ∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0
have h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜) 0
Tactic: convert! zero_add (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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜) 0
have h : ∀ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0
Tactic: apply Finset.sum_eq_zero
-- 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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ ⟪b k, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b k‖ : 𝕜) 2 * ⟪b j, b k⟫_𝕜 = 0
have hki : k < i
Tactic: have hki : k < i := by simpa using hki'
-- 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 ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
⊢ ⟪b k, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b k‖ : 𝕜) 2 * ⟪b j, b k⟫_𝕜 = 0
have this : ⟪b j, b k⟫_𝕜 = 0
Tactic: have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'
-- 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
i j : ι
hij : i ≤ j
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f i)
have rw : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j))
  (gramSchmidt 𝕜 f i + ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i))
Tactic: rw [gramSchmidt_def' 𝕜 f i]
-- 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
i j : ι
hij : i ≤ j
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j))
    (gramSchmidt 𝕜 f i + ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i))
have simp_rw : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j))
  (gramSchmidt 𝕜 f i +
    ∑ x ∈ Finset.Iio i,
      (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜)) • gramSchmidt 𝕜 f x)
Tactic: simp_rw [starProjection_singleton]