𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) ↔
    ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ Orthonormal 𝕜 Subtype.val ↔ ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
rw [orthonormal_iff_ite]
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) →
    ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (v : E), v ∈ s → ∀ (w : E), 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
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) ↔
    ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
constructor
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
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
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), inner ↑i ↑j = if i = j then 1 else 0) →
    ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
intro h v hv w hw
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
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 { val := v, property := hv } = { val := w, property := hw } then 1 else 0
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
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
convert h ⟨v, hv⟩ ⟨w, hw⟩ using 1
no goals
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
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 { val := v, property := hv } = { val := w, property := hw } then 1 else 0
simp
case mpr.mk.mk
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
h : ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner ↑{ val := v, property := hv } ↑{ val := w, property := hw } =
    if { val := v, property := hv } = { val := w, property := hw } then 1 else 0
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
⊢ (∀ (v : E), v ∈ s → ∀ (w : E), 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
rintro h ⟨v, hv⟩ ⟨w, hw⟩
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
h : ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if { val := v, property := hv } = { val := w, property := hw } then 1 else 0) = if v = w then 1 else 0
case mpr.mk.mk
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
h : ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ inner ↑{ val := v, property := hv } ↑{ val := w, property := hw } =
    if { val := v, property := hv } = { val := w, property := hw } then 1 else 0
convert h v hv w hw using 1
no goals
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.1899983
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.1900032
dec_ι : DecidableEq ι
s : Set E
h : ∀ (v : E), v ∈ s → ∀ (w : E), w ∈ s → inner v w = if v = w then 1 else 0
v : E
hv : v ∈ s
w : E
hw : w ∈ s
⊢ (if { val := v, property := hv } = { val := w, property := hw } then 1 else 0) = if v = w then 1 else 0
simp