-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_subtype_iff_ite [DecidableEq E] {s : Set E} :
    Orthonormal 𝕜 (Subtype.val : s → E) ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner v w = if v = w then 1 else 0

Tactic:
convert h ⟨v, hv⟩ ⟨w, hw⟩ using 1

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if v = w then 1 else 0) = if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) →
    ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0

Tactic:
intro h v hv w hw

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner v w = if v = w then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0

Tactic:
rw [orthonormal_iff_ite]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) ↔
    ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) ↔
    ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) →
    ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0) →
    ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0) = if v = w then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if v = w then 1 else 0) = if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case mpr.mk.mk
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner ↑⟨v, hv⟩ ↑⟨w, hw⟩ = if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0

Tactic:
convert h v hv w hw using 1

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0) = if v = w then 1 else 0

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0) →
    ∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0

Tactic:
rintro h ⟨v, hv⟩ ⟨w, hw⟩

Result:
case mpr.mk.mk
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
h : ∀ v ∈ s, ∀ w ∈ s, inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner ↑⟨v, hv⟩ ↑⟨w, hw⟩ = if ⟨v, hv⟩ = ⟨w, hw⟩ then 1 else 0