awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : v ∈ Kᗮᗮ → v ∈ K
h₁ : v ∈ K → v ∈ Kᗮᗮ
⊢ v ∈ Kᗮᗮ ↔ v ∈ K

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : ∀ (y : E) (hy : y ∈ K) (z : E) (hz : z ∈ Kᗮ), y + z ∈ Kᗮᗮ → y + z ∈ K
⊢ v ∈ Kᗮᗮ → v ∈ K

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_add_mem_mem_orthogonal v

Premises used: Submodule.exists_add_mem_mem_orthogonal, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ ⟪z, y⟫ = 0

Tactic:
simp [hz y hy, inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ ⟪z, y⟫ = 0

Tactic:
have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hyz : ⟪z, y⟫ = 0
⊢ z = 0

Tactic:
simpa [inner_add_right, hyz] using hv z hz

Premises used: inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ z = 0

Tactic:
have hz' : z = 0 := by
      have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
      simpa [inner_add_right, hyz] using hv z hz
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hz' : z = 0
⊢ y + z ∈ K

Tactic:
simp [hy, hz']
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
h : ⟪v, w⟫ = 0
⊢ ⟪w, v⟫ = 0

Tactic:
rw [inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ ⟪v, w⟫ = 0

Tactic:
hw v hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ ⟪v, w⟫ = 0

Tactic:
exact hw v hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
h : K₀ᗮ ≤ K₁ᗮ
⊢ K₁ ≤ K₀

Tactic:
simpa using orthogonal_le h

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
rw : K₁ᗮ ≤ K₀ᗮᗮ ↔ K₁ᗮ ≤ K₀
rw₁ rw₂ : K₁ᗮ ≤ K₀ ↔ K₁ᗮ ≤ K₀
⊢ K₀ᗮ ≤ K₁ ↔ K₁ᗮ ≤ K₀

Tactic:
rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]

Premises used: Submodule.orthogonal_orthogonal, Submodule.orthogonal_le_orthogonal_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₀ K₁ : Submodule 𝕜 E
inst_3 : K₀.HasOrthogonalProjection
inst_4 : K₁.HasOrthogonalProjection
rw : K₁ᗮᗮ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
rw₁ rw₂ : K₁ ≤ K₀ᗮ ↔ K₁ ≤ K₀ᗮ
⊢ K₀ ≤ K₁ᗮ ↔ K₁ ≤ K₀ᗮ

Tactic:
rw [← orthogonal_le_orthogonal_iff, orthogonal_orthogonal]

Premises used: Submodule.orthogonal_orthogonal, Submodule.orthogonal_le_orthogonal_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
⊢ Kᗮᗮ = K.topologicalClosure

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
refine_1 : Kᗮᗮ ≤ K.topologicalClosure
refine_2 : K.topologicalClosure ≤ Kᗮᗮ
⊢ Kᗮᗮ = K.topologicalClosure

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
⊢ Kᗮᗮ ≤ K.topologicalClosureᗮᗮ

Tactic:
Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure

Premises used: Submodule.orthogonal_orthogonal_monotone, Submodule.le_topologicalClosure
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : K.topologicalClosure = K.topologicalClosureᗮᗮ
⊢ Kᗮᗮ ≤ K.topologicalClosure

Tactic:
convert! Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure using 1

Premises used: Submodule.orthogonal_orthogonal_monotone, Submodule.le_topologicalClosure
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h h₁ : K.topologicalClosure = K.topologicalClosure
⊢ K.topologicalClosure = K.topologicalClosureᗮᗮ

Tactic:
rw [K.topologicalClosure.orthogonal_orthogonal]

Premises used: Submodule.orthogonal_orthogonal, Submodule.topologicalClosure
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
⊢ K.topologicalClosure ≤ Kᗮᗮ

Tactic:
K.topologicalClosure_minimal K.le_orthogonal_orthogonal Kᗮ.isClosed_orthogonal

Premises used: Submodule.topologicalClosure_minimal, Submodule.le_orthogonal_orthogonal, Submodule.orthogonal, Submodule.isClosed_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
⊢ K.topologicalClosure ≤ Kᗮᗮ

Tactic:
exact K.topologicalClosure_minimal K.le_orthogonal_orthogonal Kᗮ.isClosed_orthogonal

Premises used: Submodule.topologicalClosure_minimal, Submodule.le_orthogonal_orthogonal, Submodule.orthogonal, Submodule.isClosed_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ IsCompl K Kᗮ

Tactic:
⟨K.orthogonal_disjoint, codisjoint_iff.2 Submodule.sup_orthogonal_of_hasOrthogonalProjection⟩

Premises used: Iff.mpr, Submodule.orthogonal_disjoint, codisjoint_iff, Submodule.sup_orthogonal_of_hasOrthogonalProjection, IsCompl.mk
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K L : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
inst_4 : L.HasOrthogonalProjection
h : Kᗮ = Lᗮ
⊢ K = L

Tactic:
simpa using congr(Submodule.orthogonal $(h))
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h : K = ⊤
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ Kᗮ = ⊥

Tactic:
rw [h, Submodule.top_orthogonal_eq_bot]

Premises used: Submodule.top_orthogonal_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
refine : Kᗮ = ⊥ → K = ⊤
⊢ Kᗮ = ⊥ ↔ K = ⊤

Tactic:
refine ⟨?_, fun h => by rw [h, Submodule.top_orthogonal_eq_bot]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h : Kᗮ = ⊥
⊢ K ⊔ Kᗮ = ⊤

Tactic:
have : K ⊔ Kᗮ = ⊤ := Submodule.sup_orthogonal_of_hasOrthogonalProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h : Kᗮ = ⊥
this : K ⊔ Kᗮ = ⊤
rwa : ∀ (this : K ⊔ ⊥ = ⊤), K = ⊤
rwa₁ : ∀ (this : ⊥ ⊔ K = ⊤), K = ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : K = ⊤), K = ⊤
⊢ K = ⊤

Tactic:
rwa [h, sup_comm, bot_sup_eq] at this

Premises used: bot_sup_eq, sup_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)

Tactic:
.of_neBot_imp fun h ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
⊢ NeBot.{u_4} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun h ↦ ?_
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
⊢ Nonempty ι

Tactic:
cases atTop_neBot_iff.mp h

Premises used: Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
⊢ IsDirectedOrder ι

Tactic:
cases atTop_neBot_iff.mp h

Premises used: Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
⊢ ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))

Tactic:
have proj_x : ∀ i, (U i).orthogonalProjection x = (U i).orthogonalProjection y := fun i =>
    (orthogonalProjection_starProjection_of_le
        ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
this : ∀ ε > 0, ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)

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

Premises used: Submodule.starProjection_apply, NormedAddCommGroup.tendsto_atTop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
intro : ∀ ε > 0, ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)

Tactic:
suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(U i).starProjection y - y‖ < ε by
    simpa only [starProjection_apply, proj_x, NormedAddCommGroup.tendsto_atTop] using this
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (topologicalClosure (⨆ (i : ι), U i)) y

Tactic:
have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
y_mem : Membership.mem (γ := Submodule 𝕜 E) (topologicalClosure (⨆ (i : ι), U i)) y
⊢ ∀ ε > 0, ∃ b ∈ (↑(⨆ (i : ι), U i) : Set E), dist y b < ε

Tactic:
rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem

Premises used: Metric.mem_closure_iff, Submodule.topologicalClosure_coe, SetLike.mem_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
y_mem : ∀ ε > 0, ∃ b ∈ (↑(⨆ (i : ι), U i) : Set E), dist y b < ε
⊢ ∃ (a : E), Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a ∧ dist y a < ε

Tactic:
y_mem ε hε
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
y_mem : ∀ ε > 0, ∃ b ∈ (↑(⨆ (i : ι), U i) : Set E), dist y b < ε
⊢ ∃ (a : E), Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a ∧ dist y a < ε

Tactic:
exact y_mem ε hε
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
intro :
  ∀ (a : E) (ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a) (hay : dist y a < ε),
    ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) 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ε
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : dist y a < ε
⊢ ‖y - a‖ < ε

Tactic:
rw [dist_eq_norm] at hay

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
rwa rwa₁ rwa₂ rwa₃ : ∀ (ha : ∃ (i : ι), a ∈ U i) (hay : ‖y - a‖ < ε), ∃ (I : ι), a ∈ U I
⊢ ∃ (I : ι), a ∈ U I

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

Premises used: Monotone.directed_le, Submodule.mem_iSup_of_directed
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
intro :
  ∀ (I : ι) (hI : a ∈ U I), ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε

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

Premises used: RCLike.I