awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
neg neg₁ neg₂ neg₃ : gramSchmidt 𝕜 f a ≠ 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0

Tactic:
rwa [inner_self_ne_zero]

Premises used: inner_self_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
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
⊢ ⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f i‖ 2) : 𝕜) *
      ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 =
    0

Tactic:
simp only [mul_eq_zero, div_eq_zero_iff]

Premises used: mul_eq_zero, div_eq_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 : ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
⊢ (⟪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:
right
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
h₁ : ∀ (hia₂ : a < i), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
rcases hia.lt_or_gt with hia₁ | hia₂

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
h : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f a⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
rw [inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 i, gramSchmidt 𝕜 f a⟫_𝕜 = 0

Tactic:
ih a h₀ i hia₁
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 i, gramSchmidt 𝕜 f a⟫_𝕜 = 0

Tactic:
exact ih a h₀ i hia₁
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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₂ : a < i
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
ih i (mem_Iio.1 hi) a hia₂

Premises used: Iff.mp, Finset.mem_Iio
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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₂ : a < i
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
exact ih i (mem_Iio.1 hi) a hia₂

Premises used: Iff.mp, Finset.mem_Iio
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
⊢ Pairwise fun (a b : ι) ↦ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
fun _ _ =>
  gramSchmidt_orthogonal 𝕜 f

Premises used: InnerProductSpace.gramSchmidt_orthogonal, Pairwise
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
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
⊢ ⟪gramSchmidt 𝕜 v j, v i⟫_𝕜 = 0

Tactic:
rw [gramSchmidt_def'' 𝕜 v]

Premises used: InnerProductSpace.gramSchmidt_def''
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
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
⊢ ⟪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:
simp only [inner_add_right, inner_sum, inner_smul_right]

Premises used: inner_sum, inner_add_right, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
set :
  let b := gramSchmidt 𝕜 v;
  ⟪b j, b i⟫_𝕜 + ∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0
⊢ ⟪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:
set b : ι → E := gramSchmidt 𝕜 v

Premises used: InnerProductSpace.gramSchmidt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
⊢ HAdd.hAdd (α := 𝕜) 0 0 = 0

Tactic:
zero_add (0 : 𝕜)

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜) 0
⊢ ⟪b j, b i⟫_𝕜 + ∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0

Tactic:
convert! zero_add (0 : 𝕜)

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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⟫_𝕜 = 0

Tactic:
gramSchmidt_orthogonal 𝕜 v hij.ne'

Premises used: InnerProductSpace.gramSchmidt_orthogonal, LT.lt.ne'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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⟫_𝕜 = 0

Tactic:
exact gramSchmidt_orthogonal 𝕜 v hij.ne'

Premises used: InnerProductSpace.gramSchmidt_orthogonal, LT.lt.ne'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 : ∀ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜 = 0
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b x‖ : 𝕜) 2 * ⟪b j, b x⟫_𝕜) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
⊢ k < i

Tactic:
simpa using hki'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
⊢ k < i

Tactic:
have hki : k < i := by simpa using hki'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 j, b k⟫_𝕜 = 0

Tactic:
have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
this : ⟪b j, b k⟫_𝕜 = 0
⊢ ⟪b k, v i⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖b k‖ : 𝕜) 2 * ⟪b j, b k⟫_𝕜 = 0

Tactic:
simp [this]
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
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))
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f i)

Tactic:
rw [gramSchmidt_def' 𝕜 f i]

Premises used: InnerProductSpace.gramSchmidt_def'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
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)
⊢ 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:
simp_rw [starProjection_singleton]

Premises used: Submodule.starProjection_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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 +
      ∑ x ∈ Finset.Iio i,
        (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜)) • gramSchmidt 𝕜 f x)

Tactic:
Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
    (Submodule.sum_mem _ fun k hk => smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
      subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)

Premises used: Norm.norm, Inner.inner, Submodule.sum_mem, HDiv.hDiv, LT.lt.le, RCLike.ofReal, InnerProductSpace.gramSchmidt, HPow.hPow, Set.mem_image_of_mem, Submodule.span, Iff.mp, Set.image, Set.Iic, Submodule.subset_span, LE.le.trans, Finset.mem_Iio, OfNat.ofNat, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
rw :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    (f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i))
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j)) (gramSchmidt 𝕜 f i)

Tactic:
rw [gramSchmidt_def 𝕜 f i]

Premises used: InnerProductSpace.gramSchmidt_def
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
simp_rw :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    (f i -
      ∑ x ∈ Finset.Iio i,
        (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜)) • gramSchmidt 𝕜 f x)
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    (f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i))

Tactic:
simp_rw [starProjection_singleton]

Premises used: Submodule.starProjection_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    (f i -
      ∑ x ∈ Finset.Iio i,
        (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜)) • gramSchmidt 𝕜 f x)

Tactic:
Submodule.sub_mem _ (subset_span (mem_image_of_mem _ hij))
    (Submodule.sum_mem _ fun k hk => ?_)

Premises used: Set.Mem, Submodule.sum_mem, Set.mem_image_of_mem, Submodule.subset_span, Submodule.sub_mem
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
refine :
  ∀ (k : ι) (hk : k ∈ Finset.Iio i),
    Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
      ((⟪gramSchmidt 𝕜 f k, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f k‖ 2) : 𝕜)) • gramSchmidt 𝕜 f k)
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    (f i -
      ∑ x ∈ Finset.Iio i,
        (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜)) • gramSchmidt 𝕜 f x)

Tactic:
refine Submodule.sub_mem _ (subset_span (mem_image_of_mem _ hij))
    (Submodule.sum_mem _ fun k hk => ?_)

Premises used: Submodule.sum_mem, Set.mem_image_of_mem, Submodule.subset_span, Submodule.sub_mem
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
k : ι
hk : k ∈ Finset.Iio i
hkj : k < j := ⋯
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    ((⟪gramSchmidt 𝕜 f k, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f k‖ 2) : 𝕜)) • gramSchmidt 𝕜 f k)

Tactic:
smul_mem _ _
    (span_mono (image_mono <| Set.Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)

Premises used: Iff.mpr, le_rfl, Set.Mem, Set.Iic_subset_Iic, Set.image_mono, LT.lt.le, Submodule.span_mono, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
j i : ι
hij : i ≤ j
k : ι
hk : k ∈ Finset.Iio i
hkj : k < j := ⋯
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (f '' Set.Iic j))
    ((⟪gramSchmidt 𝕜 f k, f i⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f k‖ 2) : 𝕜)) • gramSchmidt 𝕜 f k)

Tactic:
exact smul_mem _ _
    (span_mono (image_mono <| Set.Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)

Premises used: Iff.mpr, le_rfl, Set.Iic_subset_Iic, Set.image_mono, LT.lt.le, Submodule.span_mono, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
c : ι
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic c)) (span 𝕜 (f '' Set.Iic c))

Tactic:
span_eq_span (Set.image_subset_iff.2 fun _ => gramSchmidt_mem_span _ _) <|
    Set.image_subset_iff.2 fun _ => mem_span_gramSchmidt _ _

Premises used: Iff.mpr, InnerProductSpace.mem_span_gramSchmidt, Set.image_subset_iff, Submodule.span_eq_span, InnerProductSpace.gramSchmidt_mem_span
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
c : ι
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio c)) (span 𝕜 (f '' Set.Iio c))

Tactic:
span_eq_span (Set.image_subset_iff.2 fun _ hi =>
    span_mono (image_mono <| Iic_subset_Iio.2 hi) <| gramSchmidt_mem_span _ _ le_rfl) <|
      Set.image_subset_iff.2 fun _ hi =>
        span_mono (image_mono <| Iic_subset_Iio.2 hi) <| mem_span_gramSchmidt _ _ le_rfl

Premises used: Iff.mpr, le_rfl, Set.image_mono, Set.Iic_subset_Iio, InnerProductSpace.mem_span_gramSchmidt, Submodule.span_mono, Set.image_subset_iff, Submodule.span_eq_span, InnerProductSpace.gramSchmidt_mem_span
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range (gramSchmidt 𝕜 f))) (span 𝕜 (Set.range f))

Tactic:
span_eq_span (range_subset_iff.2 fun _ =>
    span_mono (image_subset_range _ _) <| gramSchmidt_mem_span _ _ le_rfl) <|
      range_subset_iff.2 fun _ =>
        span_mono (image_subset_range _ _) <| mem_span_gramSchmidt _ _ le_rfl

Premises used: Iff.mpr, le_rfl, Set.image_subset_range, InnerProductSpace.gramSchmidt, InnerProductSpace.mem_span_gramSchmidt, Submodule.span_mono, Set.Iic, Set.range_subset_iff, Submodule.span_eq_span, InnerProductSpace.gramSchmidt_mem_span
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
hf : Pairwise fun (x1 x2 : ι) ↦ ⟪f x1, f x2⟫_𝕜 = 0
h : ∀ (i : ι), gramSchmidt 𝕜 f i = f i
⊢ gramSchmidt 𝕜 f = f

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
hf : Pairwise fun (x1 x2 : ι) ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
h : f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i) = f i
⊢ gramSchmidt 𝕜 f i = f i

Tactic:
rw [gramSchmidt_def]

Premises used: InnerProductSpace.gramSchmidt_def
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
hf : Pairwise fun (x1 x2 : ι) ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
trans : f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i) = f i - 0
trans₁ : f i - 0 = f i
⊢ f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i) = f i

Tactic:
trans f i - 0
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
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
hf : Pairwise fun (x1 x2 : ι) ↦ ⟪f x1, f x2⟫_𝕜 = 0
i : ι
e_a : Eq.{u_2 + 1} (α := E) (∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i)) 0
⊢ f i - ∑ i_1 ∈ Finset.Iio i, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i_1) : (a : E) → E) (f i) = f i - 0

Tactic:
congr