𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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})
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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)
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) _)
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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})
simp only [coe_singleton, Set.image_singleton]
case pos
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}

case neg
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}
by_cases h : gramSchmidt 𝕜 f i = 0
no goals
case pos
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}
simp [h]
case neg
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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
case neg
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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}
refine' mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ _ _⟩
no goals
case neg
𝕜 : Type u_3
E : Type u_2
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
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
exact_mod_cast norm_ne_zero_iff.2 h