𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ False
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ gramSchmidt 𝕜 f n ≠ 0
by_contra h
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
⊢ False
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ False
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⟩
𝕜 : Type u_2
E : Type u_3
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
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) }
𝕜 : Type u_2
E : Type u_3
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
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
apply LinearIndependent.not_mem_span_image h₀ _ h₂
no goals
𝕜 : Type u_2
E : Type u_3
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
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) }
simp only [Set.mem_Iio, lt_self_iff_false, not_false_iff]
𝕜 : Type u_2
E : Type u_3
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
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)
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ f n ∈ span 𝕜 (f '' Set.Iio n)
rw [← span_gramSchmidt_Iio 𝕜 f n, gramSchmidt_def' 𝕜 f, h, zero_add]
𝕜 : Type u_2
E : Type u_3
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
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)
𝕜 : Type u_2
E : Type u_3
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
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)
apply Submodule.sum_mem _ _
𝕜 : Type u_2
E : Type u_3
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
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)
𝕜 : Type u_2
E : Type u_3
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
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)
intro a ha
𝕜 : Type u_2
E : Type u_3
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
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)
𝕜 : Type u_2
E : Type u_3
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
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)
simp only [Set.mem_image, Set.mem_Iio, orthogonalProjection_singleton]
𝕜 : Type u_2
E : Type u_3
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
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)
𝕜 : Type u_2
E : Type u_3
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
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)
apply Submodule.smul_mem _ _ _
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
𝕜 : Type u_2
E : Type u_3
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
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)
rw [Finset.mem_Iio] at ha
no goals
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
refine' subset_span ⟨a, ha, by rfl⟩
no goals
𝕜 : Type u_2
E : Type u_3
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
ha : a < n
⊢ gramSchmidt 𝕜 f a = gramSchmidt 𝕜 f a
rfl
𝕜 : Type u_2
E : Type u_3
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
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) }))
𝕜 : Type u_2
E : Type u_3
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
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) })
rw [image_comp]
case h.e'_5.h.e'_6.h.e'_4
𝕜 : Type u_2
E : Type u_3
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
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
𝕜 : Type u_2
E : Type u_3
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
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) }))
convert h₁ using 3
case h.e'_5.h.e'_6.h.e'_4.h
𝕜 : Type u_2
E : Type u_3
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
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
case h.e'_5.h.e'_6.h.e'_4
𝕜 : Type u_2
E : Type u_3
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
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
ext i
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_2
E : Type u_3
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
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

case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
case h.e'_5.h.e'_6.h.e'_4.h
𝕜 : Type u_2
E : Type u_3
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
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
apply Iff.intro <;> simp
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_2
E : Type u_3
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
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
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_2
E : Type u_3
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
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
intros
no goals
case h.e'_5.h.e'_6.h.e'_4.h.mp
𝕜 : Type u_2
E : Type u_3
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
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
simp_all only
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
intros q
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
use i
no goals
case h.e'_5.h.e'_6.h.e'_4.h.mpr
𝕜 : Type u_2
E : Type u_3
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
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
exact ⟨q, le_of_lt q, rfl⟩