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

Proof state:
case h.e'_5.h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ x = ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)

Tactic:
rw [eq_comm, orthogonalProjection_eq_self_iff, top_unique hU']

Result:
case h.e'_5.h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ 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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ Tendsto (fun t => ↑((orthogonalProjection (U t)) x)) atTop (𝓝 x)

Tactic:
convert orthogonalProjection_tendsto_closure_iSup U hU x

Result:
case h.e'_5.h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ x = ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)

Proof state:
case h.e'_5.h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ x ∈ ⊤

Tactic:
trivial

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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ Tendsto (fun t => ↑((orthogonalProjection (U t)) x)) atTop (𝓝 x)

Tactic:
have : HasOrthogonalProjection (⨆ i, U i).topologicalClosure := by
  rw [top_unique hU']
  infer_instance

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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
⊢ Tendsto (fun t => ↑((orthogonalProjection (U t)) x)) atTop (𝓝 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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ HasOrthogonalProjection (⨆ i, U i).topologicalClosure

Tactic:
rw [top_unique hU']

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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ HasOrthogonalProjection ⊤

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✝ : ∀ (t : ι), HasOrthogonalProjection (U t)
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
⊢ HasOrthogonalProjection ⊤

Tactic:
infer_instance

Result:
no goals