ι : Type u_1
ι' : Type ?u.723850
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.723859
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.723879
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.723897
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.723917
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ι → ι → True
ι : Type u_1
ι' : Type ?u.723850
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.723859
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.723879
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.723897
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.723917
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Orthonormal 𝕜 fun i => single i 1
simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
  EuclideanSpace.single_apply]
ι : Type u_1
ι' : Type ?u.723850
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.723859
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.723879
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.723897
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.723917
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i✝ j✝ : ι
⊢ True
ι : Type u_1
ι' : Type ?u.723850
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.723859
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.723879
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.723897
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.723917
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ι → ι → True
intros
no goals
ι : Type u_1
ι' : Type ?u.723850
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.723859
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.723879
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.723897
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.723917
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i✝ j✝ : ι
⊢ True
trivial