𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 fun x => ↑x
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x
classical!
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
⊢ ∀ (v : E), (v ∈ ⋃ (i : η), s i) → ∀ (w : E), (w ∈ ⋃ (i : η), s i) → inner v w = if v = w then 1 else 0
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 fun x => ↑x
rw [orthonormal_subtype_iff_ite]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
⊢ inner x y = if x = y then 1 else 0
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
⊢ ∀ (v : E), (v ∈ ⋃ (i : η), s i) → ∀ (w : E), (w ∈ ⋃ (i : η), s i) → inner v w = if v = w then 1 else 0
rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ inner x y = if x = y then 1 else 0
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
⊢ inner x y = if x = y then 1 else 0
obtain ⟨k, hik, hjk⟩ := hs i j
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : Orthonormal 𝕜 fun x => ↑x
⊢ inner x y = if x = y then 1 else 0
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ inner x y = if x = y then 1 else 0
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : ∀ (v : E), v ∈ s k → ∀ (w : E), w ∈ s k → inner v w = if v = w then 1 else 0
⊢ inner x y = if x = y then 1 else 0
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : Orthonormal 𝕜 fun x => ↑x
⊢ inner x y = if x = y then 1 else 0
rw [orthonormal_subtype_iff_ite] at h_orth
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_2
F : Type ?u.2157354
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2157403
dec_ι : DecidableEq ι
η : Type u_1
s : η → Set E
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
em✝ : (a : Prop) → Decidable a
x : E
i : η
hxi : x ∈ (fun i => s i) i
y : E
j : η
hyj : y ∈ (fun i => s i) j
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : ∀ (v : E), v ∈ s k → ∀ (w : E), w ∈ s k → inner v w = if v = w then 1 else 0
⊢ inner x y = if x = y then 1 else 0
exact h_orth x (hik hxi) y (hjk hyj)