[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
n : ι
i : { x // x ∈ Iio n }
⊢ (invImage (fun a => a) IsWellOrder.toHasWellFounded).1 (↑i) n
[PROOFSTEP]
exact mem_Iio.1 i.2
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
⊢ gramSchmidt 𝕜 f n = f n - ∑ i in Iio n, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
[PROOFSTEP]
rw [← sum_attach, attach_eq_univ, gramSchmidt]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
⊢ f n = gramSchmidt 𝕜 f n + ∑ i in Iio n, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
[PROOFSTEP]
rw [gramSchmidt_def, sub_add_cancel]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
⊢ f n =
    gramSchmidt 𝕜 f n + ∑ i in Iio n, (inner (gramSchmidt 𝕜 f i) (f n) / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i
[PROOFSTEP]
convert gramSchmidt_def' 𝕜 f n
[GOAL]
case h.e'_3.h.e'_6.a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n x✝ : ι
a✝ : x✝ ∈ Iio n
⊢ (inner (gramSchmidt 𝕜 f x✝) (f n) / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ =
    ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))
[PROOFSTEP]
rw [orthogonalProjection_singleton, IsROrC.ofReal_pow]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
ι✝ : Type u_3
inst✝⁶ : LinearOrder ι✝
inst✝⁵ : LocallyFiniteOrderBot ι✝
inst✝⁴ : IsWellOrder ι✝ fun x x_1 => x < x_1
ι : Type u_4
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : OrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥
[PROOFSTEP]
rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
suffices ∀ a b : ι, a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0
  by
  cases' h₀.lt_or_lt with ha hb
  · exact this _ _ ha
  · rw [inner_eq_zero_symm]
    exact this _ _ hb
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
cases' h₀.lt_or_lt with ha hb
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
ha : a < b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
exact this _ _ ha
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
hb : b < a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
rw [inner_eq_zero_symm]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
hb : b < a
⊢ inner (gramSchmidt 𝕜 f b) (gramSchmidt 𝕜 f a) = 0
[PROOFSTEP]
exact this _ _ hb
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a ≠ b
⊢ ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
clear h₀ a b
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ ∀ (a b : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
intro a b h₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
a b : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
revert a
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b : ι
⊢ ∀ (a : ι), a < b → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
apply WellFounded.induction (@IsWellFounded.wf ι (· < ·) _) b
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b : ι
⊢ ∀ (x : ι),
    (∀ (y : ι), y < x → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0) →
      ∀ (a : ι), a < x → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f x) = 0
[PROOFSTEP]
intro b ih a h₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b) = 0
[PROOFSTEP]
simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum, orthogonalProjection_singleton, inner_smul_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      ∑ x in Iio b,
        inner (gramSchmidt 𝕜 f x) (f b) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f x) =
    0
[PROOFSTEP]
rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr h₀)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0
[PROOFSTEP]
by_cases h : gramSchmidt 𝕜 f a = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
h : gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0
[PROOFSTEP]
simp only [h, inner_zero_left, zero_div, zero_mul, sub_zero]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (f b) -
      inner (gramSchmidt 𝕜 f a) (f b) / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) =
    0
[PROOFSTEP]
rw [IsROrC.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel, sub_self]
[GOAL]
case neg.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f a) ≠ 0
[PROOFSTEP]
rwa [inner_self_ne_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
⊢ ∀ (b_1 : ι),
    b_1 ∈ Iio b →
      b_1 ≠ a →
        inner (gramSchmidt 𝕜 f b_1) (f b) / ↑(‖gramSchmidt 𝕜 f b_1‖ ^ 2) *
            inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f b_1) =
          0
[PROOFSTEP]
intro i hi hia
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ inner (gramSchmidt 𝕜 f i) (f b) / ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) * inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0
[PROOFSTEP]
simp only [mul_eq_zero, div_eq_zero_iff, inner_self_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ (inner (gramSchmidt 𝕜 f i) (f b) = 0 ∨ ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) = 0) ∨
    inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0
[PROOFSTEP]
right
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0
[PROOFSTEP]
cases' hia.lt_or_lt with hia₁ hia₂
[GOAL]
case h.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0
[PROOFSTEP]
rw [inner_eq_zero_symm]
[GOAL]
case h.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₁ : i < a
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f a) = 0
[PROOFSTEP]
exact ih a h₀ i hia₁
[GOAL]
case h.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
b✝ b : ι
ih : ∀ (y : ι), y < b → ∀ (a : ι), a < y → inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f y) = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₂ : a < i
⊢ inner (gramSchmidt 𝕜 f a) (gramSchmidt 𝕜 f i) = 0
[PROOFSTEP]
exact ih i (mem_Iio.1 hi) a hia₂
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j) (v i) = 0
[PROOFSTEP]
rw [gramSchmidt_def'' 𝕜 v]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j)
      (gramSchmidt 𝕜 v i +
        ∑ i_1 in Iio i, (inner (gramSchmidt 𝕜 v i_1) (v i) / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1) =
    0
[PROOFSTEP]
simp only [inner_add_right, inner_sum, inner_smul_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
⊢ inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v i) +
      ∑ x in Iio i,
        inner (gramSchmidt 𝕜 v x) (v i) / ↑‖gramSchmidt 𝕜 v x‖ ^ 2 * inner (gramSchmidt 𝕜 v j) (gramSchmidt 𝕜 v x) =
    0
[PROOFSTEP]
set b : ι → E := gramSchmidt 𝕜 v
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) + ∑ x in Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0
[PROOFSTEP]
convert zero_add (0 : 𝕜)
[GOAL]
case h.e'_2.h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ inner (b j) (b i) = 0
[PROOFSTEP]
exact gramSchmidt_orthogonal 𝕜 v hij.ne'
[GOAL]
case h.e'_2.h.e'_6
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∑ x in Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∀ (x : ι), x ∈ Iio i → inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0
[PROOFSTEP]
rintro k hki'
[GOAL]
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0
[PROOFSTEP]
have hki : k < i := by simpa using hki'
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ k < i
[PROOFSTEP]
simpa using hki'
[GOAL]
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0
[PROOFSTEP]
have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'
[GOAL]
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
hki : k < i
this : inner (b j) (b k) = 0
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0
[PROOFSTEP]
simp [this]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
[PROOFSTEP]
rw [gramSchmidt_def' 𝕜 f i]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
[PROOFSTEP]
simp_rw [orthogonalProjection_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i +
      ∑ x in Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
[PROOFSTEP]
exact
  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)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ ∀ {j i : ι}, i ≤ j → gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
intro j i hij
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
j i : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
rw [gramSchmidt_def 𝕜 f i]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
j i : ι
hij : i ≤ j
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈ span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
simp_rw [orthogonalProjection_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
j i : ι
hij : i ≤ j
⊢ f i - ∑ x in Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
refine' Submodule.sub_mem _ (subset_span (mem_image_of_mem _ hij)) (Submodule.sum_mem _ fun k hk => _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
j i : ι
hij : i ≤ j
k : ι
hk : k ∈ Finset.Iio i
⊢ (inner (gramSchmidt 𝕜 f k) (f i) / ↑(‖gramSchmidt 𝕜 f k‖ ^ 2)) • gramSchmidt 𝕜 f k ∈ span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
j i : ι
hij : i ≤ j
k : ι
hk : k ∈ Finset.Iio i
hkj : k < j := LT.lt.trans_le (Iff.mp Finset.mem_Iio hk) hij
⊢ (inner (gramSchmidt 𝕜 f k) (f i) / ↑(‖gramSchmidt 𝕜 f k‖ ^ 2)) • gramSchmidt 𝕜 f k ∈ span 𝕜 (f '' Set.Iic j)
[PROOFSTEP]
exact smul_mem _ _ (span_mono (image_subset f <| Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
_x✝ : (j : ι) ×' (i : ι) ×' i ≤ j
a✝² :
  ∀ (y : (j : ι) ×' (i : ι) ×' i ≤ j),
    (invImage (fun a => PSigma.casesOn a fun j snd => PSigma.casesOn snd fun i snd => j) IsWellOrder.toHasWellFounded).1
        y _x✝ →
      gramSchmidt 𝕜 f y.2.1 ∈ span 𝕜 (f '' Set.Iic y.1)
j : ι
i✝ : (i : ι) ×' i ≤ j
a✝¹ :
  ∀ (y : (j : ι) ×' (i : ι) ×' i ≤ j),
    (invImage (fun a => PSigma.casesOn a fun j snd => PSigma.casesOn snd fun i snd => j) IsWellOrder.toHasWellFounded).1
        y { fst := j, snd := i✝ } →
      gramSchmidt 𝕜 f y.2.1 ∈ span 𝕜 (f '' Set.Iic y.1)
i : ι
hij : i ≤ j
a✝ :
  ∀ (y : (j : ι) ×' (i : ι) ×' i ≤ j),
    (invImage (fun a => PSigma.casesOn a fun j snd => PSigma.casesOn snd fun i snd => j) IsWellOrder.toHasWellFounded).1
        y { fst := j, snd := { fst := i, snd := hij } } →
      gramSchmidt 𝕜 f y.2.1 ∈ span 𝕜 (f '' Set.Iic y.1)
k : ι
hk : k ∈ Finset.Iio i
hkj : k < j := LT.lt.trans_le (Iff.mp Finset.mem_Iio hk) hij
⊢ (invImage (fun a => PSigma.casesOn a fun j snd => PSigma.casesOn snd fun i snd => j) IsWellOrder.toHasWellFounded).1
    { fst := k, snd := { fst := k, snd := (_ : k ≤ k) } } { fst := j, snd := { fst := i, snd := hij } }
[PROOFSTEP]
exact hkj
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
⊢ gramSchmidt 𝕜 f = f
[PROOFSTEP]
ext i
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ gramSchmidt 𝕜 f i = f i
[PROOFSTEP]
rw [gramSchmidt_def]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i
[PROOFSTEP]
trans f i - 0
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = f i - 0
[PROOFSTEP]
congr
[GOAL]
case e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∑ i_1 in Finset.Iio i, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) = 0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ ∀ (x : ι), x ∈ Finset.Iio i → ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x})) (f i)) = 0
[PROOFSTEP]
intro j hj
[GOAL]
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i)) = 0
[PROOFSTEP]
rw [coe_eq_zero]
[GOAL]
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0
[PROOFSTEP]
suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
  by
  apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
  rw [mem_orthogonal_singleton_iff_inner_left]
  rw [← mem_orthogonal_singleton_iff_inner_right]
  exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ ↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f j})) (f i) = 0
[PROOFSTEP]
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
[GOAL]
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ f i ∈ (span 𝕜 {gramSchmidt 𝕜 f j})ᗮ
[PROOFSTEP]
rw [mem_orthogonal_singleton_iff_inner_left]
[GOAL]
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ inner (f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
rw [← mem_orthogonal_singleton_iff_inner_right]
[GOAL]
case hv
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
⊢ gramSchmidt 𝕜 f j ∈ (span 𝕜 {f i})ᗮ
[PROOFSTEP]
exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
[GOAL]
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ span 𝕜 (f '' Set.Iic j) ⟂ span 𝕜 {f i}
[PROOFSTEP]
rw [isOrtho_span]
[GOAL]
case e_a.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
⊢ ∀ ⦃u : E⦄, u ∈ f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {f i} → inner u v = 0
[PROOFSTEP]
rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)
[GOAL]
case e_a.h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ inner (f k) (f i) = 0
[PROOFSTEP]
apply hf
[GOAL]
case e_a.h.intro.intro.a
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i j : ι
hj : j ∈ Finset.Iio i
k : ι
hk : k ∈ Set.Iic j
⊢ k ≠ i
[PROOFSTEP]
exact (lt_of_le_of_lt hk (Finset.mem_Iio.mp hj)).ne
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
⊢ f i - 0 = f i
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ gramSchmidt 𝕜 f n ≠ 0
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ False
[PROOFSTEP]
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 
  refine' subset_span ⟨a, ha, by rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ f n ∈ span 𝕜 (f '' Set.Iio n)
[PROOFSTEP]
rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ ∑ i in Finset.Iio n, ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
[PROOFSTEP]
apply Submodule.sum_mem _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ ∀ (c : ι),
    c ∈ Finset.Iio n →
      ↑(↑(orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f c})) (f n)) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
[PROOFSTEP]
intro a ha
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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)
[PROOFSTEP]
simp only [Set.mem_image, Set.mem_Iio, orthogonalProjection_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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)
[PROOFSTEP]
apply Submodule.smul_mem _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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)
[PROOFSTEP]
rw [Finset.mem_Iio] at ha 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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)
[PROOFSTEP]
refine' subset_span ⟨a, ha, by rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a = gramSchmidt 𝕜 f a
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ False
[PROOFSTEP]
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]
  convert h₁ using 3
  ext i
  apply Iff.intro <;>
    simp
      -- Porting note: was `simpa using @le_of_lt _ _ i n`
  · intros; simp_all only
  · intros q; use i; exact ⟨q, le_of_lt q, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ (f ∘ Subtype.val) { val := n, property := (_ : n ≤ n) } ∈
    span 𝕜 (f ∘ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) })
[PROOFSTEP]
rw [image_comp]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ (f ∘ Subtype.val) { val := n, property := (_ : n ≤ n) } ∈
    span 𝕜 (f '' (Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) }))
[PROOFSTEP]
convert h₁ using 3
[GOAL]
case h.e'_5.h.e'_6.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) } = Set.Iio n
[PROOFSTEP]
ext i
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
⊢ i ∈ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) } ↔ i ∈ Set.Iio n
[PROOFSTEP]
apply Iff.intro
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
⊢ i ∈ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) } → i ∈ Set.Iio n
[PROOFSTEP]
simp
  -- Porting note: was `simpa using @le_of_lt _ _ i n`
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
⊢ i ∈ Set.Iio n → i ∈ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) }
[PROOFSTEP]
simp
  -- Porting note: was `simpa using @le_of_lt _ _ i n`
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
⊢ ∀ (x : ι), x < n → x ≤ n → x = i → i < n
[PROOFSTEP]
intros
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i x✝ : ι
a✝² : x✝ < n
a✝¹ : x✝ ≤ n
a✝ : x✝ = i
⊢ i < n
[PROOFSTEP]
simp_all only
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
⊢ i < n → ∃ a, a < n ∧ a ≤ n ∧ a = i
[PROOFSTEP]
intros q
[GOAL]
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
q : i < n
⊢ ∃ a, a < n ∧ a ≤ n ∧ a = i
[PROOFSTEP]
use i
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
i : ι
q : i < n
⊢ i < n ∧ i ≤ n ∧ i = i
[PROOFSTEP]
exact ⟨q, le_of_lt q, rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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) { val := n, property := (_ : n ≤ n) } ∈
    span 𝕜 (f ∘ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) })
⊢ False
[PROOFSTEP]
apply LinearIndependent.not_mem_span_image h₀ _ h₂
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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) { val := n, property := (_ : n ≤ n) } ∈
    span 𝕜 (f ∘ Subtype.val '' Set.Iio { val := n, property := (_ : n ≤ n) })
⊢ ¬{ val := n, property := (_ : n ≤ n) } ∈ Set.Iio { val := n, property := (_ : n ≤ n) }
[PROOFSTEP]
simp only [Set.mem_Iio, lt_self_iff_false, not_false_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
[PROOFSTEP]
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (gramSchmidt 𝕜 b '' Set.Iio j) := subset_span ((Set.mem_image _ _ _).2 ⟨i, hij, rfl⟩)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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
[PROOFSTEP]
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (b '' Set.Iio j) := by rwa [← span_gramSchmidt_Iio 𝕜 b j]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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)
[PROOFSTEP]
rwa [← span_gramSchmidt_Iio 𝕜 b j]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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
[PROOFSTEP]
have : ↑(b.repr (gramSchmidt 𝕜 b i)).support ⊆ Set.Iio j := Basis.repr_support_subset_of_mem_span b (Set.Iio j) this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
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
[PROOFSTEP]
exact (Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.not_mem_Iio_self
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1
[PROOFSTEP]
simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne.def, not_false_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
hn : gramSchmidtNormed 𝕜 f n ≠ 0
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1
[PROOFSTEP]
rw [gramSchmidtNormed] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ ‖(↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n‖ = 1
[PROOFSTEP]
rw [norm_smul_inv_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ gramSchmidt 𝕜 f n ≠ 0
[PROOFSTEP]
simpa using hn
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f)
[PROOFSTEP]
unfold Orthonormal
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ (∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1) ∧
    ∀ {i j : ι}, i ≠ j → inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0
[PROOFSTEP]
constructor
[GOAL]
case left
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ ∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1
[PROOFSTEP]
simp only [gramSchmidtNormed_unit_length, h₀, eq_self_iff_true, imp_true_iff]
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
⊢ ∀ {i j : ι}, i ≠ j → inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0
[PROOFSTEP]
intro i j hij
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidtNormed 𝕜 f i) (gramSchmidtNormed 𝕜 f j) = 0
[PROOFSTEP]
simp only [gramSchmidtNormed, inner_smul_left, inner_smul_right, IsROrC.conj_inv, IsROrC.conj_ofReal, mul_eq_zero,
  inv_eq_zero, IsROrC.ofReal_eq_zero, norm_eq_zero]
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
repeat' right
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
right
[GOAL]
case right.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f i = 0 ∨ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
right
[GOAL]
case right.h.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
right
[GOAL]
case right.h.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ inner (gramSchmidt 𝕜 f i) (gramSchmidt 𝕜 f j) = 0
[PROOFSTEP]
exact gramSchmidt_orthogonal 𝕜 f hij
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ Orthonormal 𝕜 fun i => gramSchmidtNormed 𝕜 f ↑i
[PROOFSTEP]
refine' ⟨fun i => gramSchmidtNormed_unit_length' i.prop, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ ∀ {i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}},
    i ≠ j → inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0
[PROOFSTEP]
rintro i j (hij : ¬_)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬i = j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0
[PROOFSTEP]
rw [Subtype.ext_iff] at hij 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}
hij : ¬↑i = ↑j
⊢ inner ((fun i => gramSchmidtNormed 𝕜 f ↑i) i) ((fun i => gramSchmidtNormed 𝕜 f ↑i) j) = 0
[PROOFSTEP]
simp [gramSchmidtNormed, inner_smul_left, inner_smul_right, gramSchmidt_orthogonal 𝕜 f hij]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = span 𝕜 (gramSchmidt 𝕜 f '' s)
[PROOFSTEP]
refine'
  span_eq_span (Set.image_subset_iff.2 fun i hi => smul_mem _ _ <| subset_span <| mem_image_of_mem _ hi)
    (Set.image_subset_iff.2 fun i hi => span_mono (image_subset _ <| singleton_subset_set_iff.2 hi) _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
⊢ gramSchmidt 𝕜 f i ∈ span 𝕜 (gramSchmidtNormed 𝕜 f '' ↑{i})
[PROOFSTEP]
simp only [coe_singleton, Set.image_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
⊢ gramSchmidt 𝕜 f i ∈ span 𝕜 {gramSchmidtNormed 𝕜 f i}
[PROOFSTEP]
by_cases h : gramSchmidt 𝕜 f i = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
h : gramSchmidt 𝕜 f i = 0
⊢ gramSchmidt 𝕜 f i ∈ span 𝕜 {gramSchmidtNormed 𝕜 f i}
[PROOFSTEP]
simp [h]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ gramSchmidt 𝕜 f i ∈ span 𝕜 {gramSchmidtNormed 𝕜 f i}
[PROOFSTEP]
refine' mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ _ _⟩
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ ↑‖gramSchmidt 𝕜 f i‖ ≠ 0
[PROOFSTEP]
exact_mod_cast norm_ne_zero_iff.2 h
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
f : ι → E
⊢ span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (Set.range (gramSchmidt 𝕜 f))
[PROOFSTEP]
simpa only [image_univ.symm] using span_gramSchmidtNormed f univ
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
⊢ ↑(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
[PROOFSTEP]
have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
⊢ gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
[PROOFSTEP]
rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ ↑(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
[PROOFSTEP]
rw [gramSchmidtOrthonormalBasis_apply h, H]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
hf : Pairwise fun i j => inner (f i) (f j) = 0
i : ι
hi : f i ≠ 0
H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i
⊢ gramSchmidtNormed 𝕜 f i ≠ 0
[PROOFSTEP]
simpa [H] using hi
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) i) (f j) = 0
[PROOFSTEP]
rw [← mem_orthogonal_singleton_iff_inner_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ f j ∈ (span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i})ᗮ
[PROOFSTEP]
suffices span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ gramSchmidtOrthonormalBasis h f i
  by
  apply this
  rw [span_gramSchmidtNormed]
  exact mem_span_gramSchmidt 𝕜 f le_rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i}
⊢ f j ∈ (span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i})ᗮ
[PROOFSTEP]
apply this
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i}
⊢ f j ∈ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)
[PROOFSTEP]
rw [span_gramSchmidtNormed]
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i}
⊢ f j ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
[PROOFSTEP]
exact mem_span_gramSchmidt 𝕜 f le_rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ span 𝕜 {↑(gramSchmidtOrthonormalBasis h f) i}
[PROOFSTEP]
rw [isOrtho_span]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ ∀ ⦃u : E⦄,
    u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {↑(gramSchmidtOrthonormalBasis h f) i} → inner u v = 0
[PROOFSTEP]
rintro u ⟨k, _, rfl⟩ v (rfl : v = _)
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
⊢ inner (gramSchmidtNormed 𝕜 f k) (↑(gramSchmidtOrthonormalBasis h f) i) = 0
[PROOFSTEP]
by_cases hk : gramSchmidtNormed 𝕜 f k = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
hk : gramSchmidtNormed 𝕜 f k = 0
⊢ inner (gramSchmidtNormed 𝕜 f k) (↑(gramSchmidtOrthonormalBasis h f) i) = 0
[PROOFSTEP]
rw [hk, inner_zero_left]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ inner (gramSchmidtNormed 𝕜 f k) (↑(gramSchmidtOrthonormalBasis h f) i) = 0
[PROOFSTEP]
rw [← gramSchmidtOrthonormalBasis_apply h hk]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) k) (↑(gramSchmidtOrthonormalBasis h f) i) = 0
[PROOFSTEP]
have : k ≠ i := by
  rintro rfl
  exact hk hi
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ k ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
hi : gramSchmidtNormed 𝕜 f k = 0
⊢ False
[PROOFSTEP]
exact hk hi
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f✝ f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
this : k ≠ i
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) k) (↑(gramSchmidtOrthonormalBasis h f) i) = 0
[PROOFSTEP]
exact (gramSchmidtOrthonormalBasis h f).orthonormal.2 this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) j) (f i) = 0
[PROOFSTEP]
by_cases hi : gramSchmidtNormed 𝕜 f j = 0
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : gramSchmidtNormed 𝕜 f j = 0
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) j) (f i) = 0
[PROOFSTEP]
rw [inner_gramSchmidtOrthonormalBasis_eq_zero h hi]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : ¬gramSchmidtNormed 𝕜 f j = 0
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) j) (f i) = 0
[PROOFSTEP]
simp [gramSchmidtOrthonormalBasis_apply h hi, gramSchmidtNormed, inner_smul_left, gramSchmidt_inv_triangular 𝕜 f hij]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : IsWellOrder ι fun x x_1 => x < x_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
⊢ ↑(gramSchmidtOrthonormalBasis h f).repr (f i) j = 0
[PROOFSTEP]
simpa [OrthonormalBasis.repr_apply_apply] using gramSchmidtOrthonormalBasis_inv_triangular h f hij
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : IsWellOrder ι fun x x_1 => x < x_1
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f))) f =
    ∏ i : ι, inner (↑(gramSchmidtOrthonormalBasis h f) i) (f i)
[PROOFSTEP]
convert Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
[GOAL]
case h.e'_3.a
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : IsWellOrder ι fun x x_1 => x < x_1
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) x✝) (f x✝) =
    Basis.toMatrix (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f)) f x✝ x✝
[PROOFSTEP]
exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm
