awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
have refine_1 : Kᗮᗮ ≤ K.topologicalClosure
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
⊢ Kᗮᗮ = K.topologicalClosure
have refine_2 : K.topologicalClosure ≤ Kᗮᗮ
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
have h : K.topologicalClosure = K.topologicalClosureᗮᗮ
Tactic: convert! Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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.topologicalClosureᗮᗮ
have h : K.topologicalClosure = K.topologicalClosure
Tactic: rw [K.topologicalClosure.orthogonal_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮ = ⊥
have rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
Tactic: rw [h, Submodule.top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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) ⊤ᗮ ⊥
⊢ Kᗮ = ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
Tactic: rw [h, Submodule.top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
⊢ Kᗮ = ⊥ ↔ K = ⊤
have refine : Kᗮ = ⊥ → K = ⊤
Tactic: refine ⟨?_, fun h => by rw [h, Submodule.top_orthogonal_eq_bot]⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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 = ⊤
have this : K ⊔ Kᗮ = ⊤
Tactic: have : K ⊔ Kᗮ = ⊤ := Submodule.sup_orthogonal_of_hasOrthogonalProjection
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮ = ⊤
⊢ K = ⊤
have rwa : ∀ (this : K ⊔ ⊥ = ⊤), K = ⊤
Tactic: rwa [h, sup_comm, bot_sup_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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 = ⊤
⊢ K = ⊤
have rwa₁ : ∀ (this : ⊥ ⊔ K = ⊤), K = ⊤
Tactic: rwa [h, sup_comm, bot_sup_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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 = ⊤
⊢ K = ⊤
have rwa₂ : ∀ (this : K = ⊤), K = ⊤
Tactic: rwa [h, sup_comm, bot_sup_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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)
have h : NeBot.{u_4} (α := ι) atTop
Tactic: refine .of_neBot_imp fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)
have left : Nonempty ι
Tactic: cases atTop_neBot_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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 ι
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)
have right : IsDirectedOrder ι
Tactic: cases atTop_neBot_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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))
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)
have intro : ∀ ε > 0, ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
Tactic: suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(U i).starProjection y - y‖ < ε by
    simpa only [starProjection_apply, proj_x, NormedAddCommGroup.tendsto_atTop] using this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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), Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a ∧ dist y a < ε
have y_mem : Membership.mem (γ := Submodule 𝕜 E) (topologicalClosure (⨆ (i : ι), U i)) y
Tactic: have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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
⊢ ∃ (a : E), Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a ∧ dist y a < ε
have y_mem₁ : ∀ ε > 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
Cleared hypotheses: y_mem
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
have 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‖ < ε
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ε
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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 < ε
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
have hay₁ : ‖y - a‖ < ε
Tactic: rw [dist_eq_norm] at hay
Cleared hypotheses: hay
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
⊢ ∃ (I : ι), a ∈ U I
have rwa : ∀ (ha : ∃ (i : ι), a ∈ U i) (hay : ‖y - a‖ < ε), ∃ (I : ι), a ∈ U I
Tactic: rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha
Cleared hypotheses: ha, hay
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
have intro : ∀ (I : ι) (hI : a ∈ U I), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
I : ι
hI : a ∈ U I
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
have intro : ∀ (i : ι) (hi : I ≤ i), ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
Tactic: refine ⟨I, fun i (hi : I ≤ i) => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
have intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ < ε
Tactic: rw [norm_sub_rev, starProjection_minimal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ < ε
have intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - a‖
Tactic: refine lt_of_le_of_lt ?_ hay
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - a‖
have intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U i) a sorry) : E)‖
Tactic: change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
⊢ HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
have rw : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) ⊤
Tactic: rw [top_unique hU']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (hypothesis)
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 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
⊢ Tendsto (fun (t : ι) ↦ ((U t).starProjection : (a : E) → E) x) atTop (𝓝 x)
have this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
Tactic: have : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection := by
    rw [top_unique hU']
    infer_instance
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
⊢ Tendsto (fun (t : ι) ↦ ((U t).starProjection : (a : E) → E) x) atTop (𝓝 x)
have h : x = (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
Tactic: convert! starProjection_tendsto_closure_iSup U hU x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
⊢ x = (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
have h : Membership.mem (γ := Submodule 𝕜 E) ⊤ x
Tactic: rw [eq_comm, starProjection_eq_self_iff, top_unique hU']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮ = ⊥
have rw : Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥
Tactic: rw [← K.orthogonal_orthogonal_eq_closure]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮ = ⊥
have mp : Kᗮᗮ = ⊤ → Kᗮ = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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
mp : Kᗮᗮ = ⊤ → Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥
have mpr : Kᗮ = ⊥ → Kᗮᗮ = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮᗮ = ⊤
⊢ Kᗮ = ⊥
have mp : Kᗮᗮᗮ = ⊥
Tactic: rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Submodule (goal)
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ᗮᗮ = ⊤
mp : Kᗮᗮᗮ = ⊥
⊢ Kᗮ = ⊥
have mp₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
Tactic: rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]