-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_iUnion_of_directed {η : Type*} {s : η → Set E} (hs : Directed (· ⊆ ·) s)
    (h : ∀ i, Orthonormal 𝕜 (fun x => x : s i → E)) :
    Orthonormal 𝕜 (fun x => x : (⋃ i, s i) → E)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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 ∈ s k, ∀ w ∈ s k, inner v w = if v = w then 1 else 0
⊢ inner x y = if x = y then 1 else 0

Tactic:
exact h_orth x (hik hxi) y (hjk hyj)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x

Tactic:
rw [orthonormal_subtype_iff_ite]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
⊢ ∀ v ∈ ⋃ i, s i, ∀ w ∈ ⋃ i, s i, inner v w = if v = w then 1 else 0

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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

Tactic:
rw [orthonormal_subtype_iff_ite] at h_orth

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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 ∈ s k, ∀ w ∈ s k, inner v w = if v = w then 1 else 0
⊢ inner x y = if x = y then 1 else 0

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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

Tactic:
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
⊢ ∀ v ∈ ⋃ i, s i, ∀ w ∈ ⋃ i, s i, inner v w = if v = w then 1 else 0

Tactic:
rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x

Tactic:
classical
rw [orthonormal_subtype_iff_ite]
rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
obtain ⟨k, hik, hjk⟩ := hs i j
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
rw [orthonormal_subtype_iff_ite] at h_orth
exact h_orth x (hik hxi) y (hjk hyj)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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

Tactic:
obtain ⟨k, hik, hjk⟩ := hs i j

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x
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