Theorem: repr_gramSchmidt_diagonal (CvxLean/Lib/Math/Analysis/InnerProductSpace/GramSchmidtOrtho.lean)

State before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) i = 1
Tactic:
rw [gramSchmidt_def, map_sub, Finsupp.sub_apply, Basis.repr_self, Finsupp.single_eq_same,
  sub_eq_self, map_sum, Finsupp.coe_finset_sum, Finset.sum_apply, Finset.sum_eq_zero]
State after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ ∀ x ∈ Finset.Iio i, (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) x})) (b i))) i = 0

State before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ ∀ x ∈ Finset.Iio i, (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) x})) (b i))) i = 0
Tactic:
intros j hj
State after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j ∈ Finset.Iio i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0

State before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j ∈ Finset.Iio i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0
Tactic:
rw [Finset.mem_Iio] at hj
State after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j < i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0

State before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j < i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0
Tactic:
simp [orthogonalProjection_singleton, gramSchmidt_triangular hj]
State after:
no goals