-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_iff_ite [DecidableEq ι] {v : ι → E} :
    Orthonormal 𝕜 v ↔ ∀ i j, ⟪v i, v j⟫ = if i = j then (1 : 𝕜) else (0 : 𝕜)

Proof state:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ = 1

Tactic:
have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by simp [@norm_sq_eq_inner 𝕜, h i i]

Result:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Proof state:
case mpr.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Tactic:
simpa [hij] using h i j

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ ^ 2 = 1 ^ 2

Tactic:
simp [@norm_sq_eq_inner 𝕜, h i i]

Result:
no goals

Proof state:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Tactic:
have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _

Result:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v

Tactic:
constructor

Result:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Pairwise fun i j => inner (v i) (v j) = 0

Proof state:
case mpr.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Pairwise fun i j => inner (v i) (v j) = 0

Tactic:
intro i j hij

Result:
case mpr.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ (∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0) → Orthonormal 𝕜 v

Tactic:
intro h

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ Orthonormal 𝕜 v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ (∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0) → Orthonormal 𝕜 v

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ inner (v i) (v j) = if i = j then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : i = j
⊢ inner (v i) (v j) = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ inner (v i) (v j) = 0

Proof state:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Tactic:
rwa [sq_eq_sq₀ h₁ h₂] at h'

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : i = j
⊢ inner (v i) (v j) = 1

Tactic:
simp [h, inner_self_eq_norm_sq_to_K, hv.1]

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v → ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0

Tactic:
intro hv i j

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
⊢ inner (v i) (v j) = if i = j then 1 else 0

Proof state:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Tactic:
have h₂ : (0 : ℝ) ≤ 1 := zero_le_one

Result:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : 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

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
h : ¬i = j
⊢ inner (v i) (v j) = 0

Tactic:
exact hv.2 h

Result:
no goals