𝕜 : 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
𝕜 : 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
refine' ⟨fun i => gramSchmidtNormed_unit_length' i.prop, _⟩
𝕜 : 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
𝕜 : 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
rintro i j (hij : ¬_)
𝕜 : 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
𝕜 : 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
rw [Subtype.ext_iff] at hij
no goals
𝕜 : 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
simp [gramSchmidtNormed, inner_smul_left, inner_smul_right, gramSchmidt_orthogonal 𝕜 f hij]