-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_triangular {i j : ι} (hij : i < j) (b : Basis ι 𝕜 E) :
    b.repr (gramSchmidt 𝕜 b i) j = 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0

Tactic:
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (gramSchmidt 𝕜 b '' Set.Iio j) :=
  subset_span ((Set.mem_image _ _ _).2 ⟨i, hij, 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0

Tactic:
have : ↑(b.repr (gramSchmidt 𝕜 b i)).support ⊆ Set.Iio j :=
  Basis.repr_support_subset_of_mem_span b (Set.Iio j) this

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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝¹ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)
this : ↑(b.repr (gramSchmidt 𝕜 (⇑b) i)).support ⊆ Set.Iio j
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
⊢ gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)

Tactic:
rwa [← span_gramSchmidt_Iio 𝕜 b j]

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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0

Tactic:
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (b '' Set.Iio j) := by rwa [← span_gramSchmidt_Iio 𝕜 b j]

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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
this : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝¹ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ⇑b '' Set.Iio j)
this✝ : gramSchmidt 𝕜 (⇑b) i ∈ span 𝕜 (⇑b '' Set.Iio j)
this : ↑(b.repr (gramSchmidt 𝕜 (⇑b) i)).support ⊆ Set.Iio j
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0

Tactic:
exact (Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.not_mem_Iio_self

Result:
no goals