-- Mathlib/Analysis/LocallyConvex/WeakSpace.lean
theorem Convex.toWeakSpace_closure {s : Set E} (hs : Convex ℝ s) :
    (toWeakSpace 𝕜 E) '' (closure s) = closure (toWeakSpace 𝕜 E '' s)

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
let f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 :=
  { toLinearMap := (f : E →ₗ[𝕜] 𝕜).comp ((toWeakSpace 𝕜 E).symm : WeakSpace 𝕜 E →ₗ[𝕜] E)
    cont := WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip _ }

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ ?m.26707 ∉ closure s

Tactic:
simpa using hx

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
obtain ⟨f, u, hus, hux⟩ := RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜)
  hs.closure isClosed_closure (by simpa using hx)

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
hux' : u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
have hus' : closure (toWeakSpace 𝕜 E '' s) ⊆
    {y | RCLike.reCLM.comp (f'.restrictScalars ℝ) y ≤ u} := by
  refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)
  rintro - ⟨y, hy, rfl⟩
  simpa [f'] using (hus y <| subset_closure hy).le

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
hux' : u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)
hus' : closure (⇑(toWeakSpace 𝕜 E) '' s) ⊆ {y | (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) y ≤ u}
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
hux' : u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)
⊢ Continuous fun y => u

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
hux' : u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)
⊢ ⇑(toWeakSpace 𝕜 E) '' s ⊆ {y | (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) y ≤ u}

Tactic:
rintro - ⟨y, hy, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
hux' : u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)
y : E
hy : y ∈ s
⊢ (toWeakSpace 𝕜 E) y ∈ {y | (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) y ≤ u}