-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_tendsto_closure_iSup {ι : Type*} [Preorder ι]
    (U : ι → Submodule 𝕜 E) [∀ i, HasOrthogonalProjection (U i)]
    [HasOrthogonalProjection (⨆ i, U i).topologicalClosure] (hU : Monotone U) (x : E) :
    Filter.Tendsto (fun i => (orthogonalProjection (U i) x : E)) atTop
      (𝓝 (orthogonalProjection (⨆ i, U i).topologicalClosure x : E))

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
⊢ ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Tactic:
obtain ⟨a, ha, hay⟩ : ∃ a ∈ ⨆ i, U i, dist y a < ε := by
  have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
  rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem
  exact y_mem ε hε

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : dist y a < ε
⊢ ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ < ε

Tactic:
refine lt_of_le_of_lt ?_ hay

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ ≤ ‖y - a‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
y_mem : ∀ ε > 0, ∃ b ∈ ↑(⨆ i, U i), dist y b < ε
⊢ ∃ a ∈ ⨆ i, U i, dist y a < ε

Tactic:
exact y_mem ε hε

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
⊢ ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Tactic:
refine ⟨I, fun i (hi : I ≤ i) => ?_⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Tactic:
rw [norm_sub_rev, orthogonalProjection_minimal]

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ < ε

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))