-- 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.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‖ < ε

Tactic:
obtain ⟨I, hI⟩ : ∃ I, a ∈ U I := by rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha

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, ∀ 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
y_mem : y ∈ (⨆ i, U i).topologicalClosure
⊢ ∃ a ∈ ⨆ i, U i, dist y a < ε

Tactic:
rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_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 : ∀ ε > 0, ∃ b ∈ ↑(⨆ i, U i), dist y b < ε
⊢ ∃ a ∈ ⨆ i, U i, dist y a < ε

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‖ ≤ ‖y - ↑⟨a, ⋯⟩‖

Tactic:
exact ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _

Result:
no goals

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

Tactic:
suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(orthogonalProjection (U i) y : E) - y‖ < ε by
  simpa only [proj_x, NormedAddCommGroup.tendsto_atTop] using this

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

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

Tactic:
have proj_x : ∀ i, orthogonalProjection (U i) x = orthogonalProjection (U i) y := fun i =>
  (orthogonalProjection_orthogonalProjection_of_le
      ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm

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