case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v → ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
⊢ (∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0) → Orthonormal 𝕜 v
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
constructor
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ inner (v i) (v j) = if i = j then 1 else 0
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v → ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
intro hv i j
case mp.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : i = j
⊢ inner (v i) (v j) = 1

case mp.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ inner (v i) (v j) = 0
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ inner (v i) (v j) = if i = j then 1 else 0
split_ifs with h
no goals
case mp.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : i = j
⊢ inner (v i) (v j) = 1
simp [h, inner_self_eq_norm_sq_to_K, hv.1]
no goals
case mp.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ inner (v i) (v j) = 0
exact hv.2 h
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
⊢ (∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0) → Orthonormal 𝕜 v
intro h
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i : ι), ‖v i‖ = 1

case mpr.right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ {i j : ι}, i ≠ j → inner (v i) (v j) = 0
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v
constructor
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ = 1
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i : ι), ‖v i‖ = 1
intro i
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
⊢ ‖v i‖ = 1
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ = 1
have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by simp [@norm_sq_eq_inner 𝕜, h i i]
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
h₁ : 0 ≤ ‖v i‖
⊢ ‖v i‖ = 1
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
⊢ ‖v i‖ = 1
have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
h₁ : 0 ≤ ‖v i‖
h₂ : 0 ≤ 1
⊢ ‖v i‖ = 1
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
h₁ : 0 ≤ ‖v i‖
⊢ ‖v i‖ = 1
have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
no goals
case mpr.left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
h₁ : 0 ≤ ‖v i‖
h₂ : 0 ≤ 1
⊢ ‖v i‖ = 1
rwa [sq_eq_sq h₁ h₂] at h'
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ ^ 2 = 1 ^ 2
simp [@norm_sq_eq_inner 𝕜, h i i]
case mpr.right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι
hij : i ≠ j
⊢ inner (v i) (v j) = 0
case mpr.right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ {i j : ι}, i ≠ j → inner (v i) (v j) = 0
intro i j hij
no goals
case mpr.right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1893320
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι
hij : i ≠ j
⊢ inner (v i) (v j) = 0
simpa [hij] using h i j