-- 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
⊢ ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

Tactic:
intro ε hε

Result:
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‖ < ε

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
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))

Tactic:
cases atTop_neBot_iff.mp h

Result:
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
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))

Proof state:
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‖ < ε

Tactic:
rw [dist_eq_norm] at hay

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 : ‖y - a‖ < ε
⊢ ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε

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
⊢ ∃ a ∈ ⨆ i, U i, dist y a < ε

Tactic:
have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _

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
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 : y ∈ (⨆ i, U i).topologicalClosure
⊢ ∃ a ∈ ⨆ i, U i, dist 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
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
⊢ ∃ I, a ∈ U I

Tactic:
rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha

Result:
no goals

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
this : ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖↑((orthogonalProjection (U i)) y) - y‖ < ε
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))

Tactic:
simpa only [proj_x, NormedAddCommGroup.tendsto_atTop] using this

Result:
no goals