-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_ne_zero_coe {f : ι → E} (n : ι)
    (h₀ : LinearIndependent 𝕜 (f ∘ ((↑) : Set.Iic n → ι))) : gramSchmidt 𝕜 f n ≠ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ False

Tactic:
have h₁ : f n ∈ span 𝕜 (f '' Set.Iio n) := by
  rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]
  apply Submodule.sum_mem _ _
  intro a ha
  simp only [Set.mem_image, Set.mem_Iio, orthogonalProjection_singleton]
  apply Submodule.smul_mem _ _ _
  rw [Finset.mem_Iio] at ha
  exact subset_span ⟨a, ha, by rfl⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a = gramSchmidt 𝕜 f a

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a ∈ Finset.Iio n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
rw [Finset.mem_Iio] at ha

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ False

Tactic:
have h₂ : (f ∘ ((↑) : Set.Iic n → ι)) ⟨n, le_refl n⟩ ∈
    span 𝕜 (f ∘ ((↑) : Set.Iic n → ι) '' Set.Iio ⟨n, le_refl n⟩) := by
  rw [image_comp]
  simpa using h₁

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a ∈ Finset.Iio n
⊢ ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f a})) (f n)) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
simp only [Set.mem_image, Set.mem_Iio, orthogonalProjection_singleton]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a ∈ Finset.Iio n
⊢ (inner (gramSchmidt 𝕜 f a) (f n) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2)) • gramSchmidt 𝕜 f a ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f '' (Subtype.val '' Set.Iio ⟨n, ⋯⟩))

Tactic:
simpa using h₁

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ ∀ c ∈ Finset.Iio n,
    ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f c})) (f n)) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
intro a ha

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a ∈ Finset.Iio n
⊢ ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f a})) (f n)) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
exact subset_span ⟨a, ha, by rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ f n ∈ span 𝕜 (f '' Set.Iio n)

Tactic:
rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ ∑ i ∈ Finset.Iio n, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)
⊢ False

Tactic:
apply LinearIndependent.not_mem_span_image h₀ _ h₂

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)
⊢ ⟨n, ⋯⟩ ∉ Set.Iio ⟨n, ⋯⟩