awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (m : 𝕜₃) (x : F →SWOT[σ₂₃] G),
    (m • x).comp f = HSMul.hSMul (α := 𝕜₃) ((RingHom.id 𝕜₃ : (a : 𝕜₃) → 𝕜₃) m : 𝕜₃) (x.comp f)

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
inst_32 : RingHomSurjective σ₂₃
inst_33 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (x y : E →SWOT[σ₁₂] F), g.comp (x + y) = g.comp x + g.comp y

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
inst_32 : RingHomSurjective σ₂₃
inst_33 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (m : 𝕜₂) (x : E →SWOT[σ₁₂] F), g.comp (m • x) = HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) m : 𝕜₃) (g.comp x)

Tactic:
simp [comp]

Premises used: ContinuousLinearMapWOT.comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
x : F →WOT[𝕜₂] F
simp_rw : Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x.comp x_1
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x * x_1

Tactic:
simp_rw [mul_eq_comp]

Premises used: ContinuousLinearMapWOT.mul_eq_comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
x : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x.comp x_1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
x : F →WOT[𝕜₂] F
simp_rw : Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x_1.comp x
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x_1 * x

Tactic:
simp_rw [mul_eq_comp]

Premises used: ContinuousLinearMapWOT.mul_eq_comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E_1
inst_3 : TopologicalSpace E_1
inst_4 : Module 𝕜₁_1 E_1
inst_5 : AddCommGroup F_1
inst_6 : TopologicalSpace F_1
inst_7 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst_8 : NormedField 𝕜₁
inst_9 : NormedField 𝕜₂
inst_10 : NormedField 𝕜₃
inst_11 : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_14 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_15 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_16 : AddCommGroup E
inst_17 : TopologicalSpace E
inst_18 : Module 𝕜₁ E
inst_19 : AddCommGroup F
inst_20 : TopologicalSpace F
inst_21 : Module 𝕜₂ F
inst_22 : AddCommGroup G
inst_23 : TopologicalSpace G
inst_24 : Module 𝕜₃ G
inst_25 : AddCommGroup H
inst_26 : TopologicalSpace H
inst_27 : Module 𝕜₄ H
inst_28 : IsTopologicalAddGroup F
inst_29 : ContinuousConstSMul 𝕜₂ F
inst_30 : IsTopologicalAddGroup G
inst_31 : ContinuousConstSMul 𝕜₃ G
x : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x_1.comp x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
⊢ Eq (α := Set (WeakSpace 𝕜 E)) ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)
    (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))

Tactic:
le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
    (Set.compl_subset_compl.mp fun x hx ↦ ?_)

Premises used: Continuous.continuousOn, toWeakSpaceCLM, Set.compl_subset_compl, le_antisymm, Iff.mp, ContinuousMapClass.map_continuous, ContinuousOn.image_closure
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
refine :
  ∀ (x : WeakSpace 𝕜 E)
    (hx : Membership.mem (γ := Set (WeakSpace 𝕜 E)) ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ x),
    Membership.mem (γ := Set (WeakSpace 𝕜 E)) (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ x
⊢ Eq (α := Set (WeakSpace 𝕜 E)) ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)
    (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))

Tactic:
refine le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
    (Set.compl_subset_compl.mp fun x hx ↦ ?_)

Premises used: Continuous.continuousOn, toWeakSpaceCLM, Set.compl_subset_compl, le_antisymm, Iff.mp, ContinuousMapClass.map_continuous, ContinuousOn.image_closure
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : WeakSpace 𝕜 E
hx : Membership.mem (γ := Set (WeakSpace 𝕜 E)) ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ x
obtain :
  ∀ (x : E)
    (hx :
      Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
        ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
        ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)),
    Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
      (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ
      ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
⊢ Membership.mem (γ := Set (WeakSpace 𝕜 E)) (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ x

Tactic:
obtain ⟨x, -, rfl⟩ := (toWeakSpace 𝕜 E).toEquiv.image_compl (closure s) |>.symm.subset hx

Premises used: Equiv.image_compl, Eq.subset, closure, toWeakSpace, LinearEquiv.toEquiv, Eq.symm, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
⊢ ContinuousSMul ℝ E

Tactic:
have : ContinuousSMul ℝ E := IsScalarTower.continuousSMul 𝕜
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
⊢ x ∉ closure s

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
obtain :
  ∀ (f : StrongDual 𝕜 E) (u : ℝ) (hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u)
    (hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)),
    Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
      (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ
      ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
⊢ Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)

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

Premises used: RCLike.geometric_hahn_banach_closed_point, Convex.closure, isClosed_closure
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u
hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)
f' : StrongDual.{u_1, u_2} 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (WeakSpace 𝕜 E) 𝕜 :=
    (↑f : E →ₗ[𝕜] 𝕜) ∘ₗ (↑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : WeakSpace 𝕜 E →ₗ[𝕜] E);
  { toLinearMap := __LinearMap, cont := ⋯ }
⊢ u <
    (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ)
      ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)

Tactic:
simpa [f']
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u
hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)
f' : StrongDual.{u_1, u_2} 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (WeakSpace 𝕜 E) 𝕜 :=
    (↑f : E →ₗ[𝕜] 𝕜) ∘ₗ (↑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : WeakSpace 𝕜 E →ₗ[𝕜] E);
  { toLinearMap := __LinearMap, cont := ⋯ }
⊢ u <
    (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ)
      ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)

Tactic:
have hux' : u < RCLike.reCLM.comp (f'.restrictScalars ℝ) (toWeakSpace 𝕜 E x) := by simpa [f']
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u
hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)
f' : StrongDual.{u_1, u_2} 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (WeakSpace 𝕜 E) 𝕜 :=
    (↑f : E →ₗ[𝕜] 𝕜) ∘ₗ (↑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : WeakSpace 𝕜 E →ₗ[𝕜] E);
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' :
  u <
    (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ)
      ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
⊢ Continuous (X := WeakSpace 𝕜 E) (Y := ℝ)
    (⇑(RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') : (a : WeakSpace 𝕜 E) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u
hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)
f' : StrongDual.{u_1, u_2} 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (WeakSpace 𝕜 E) 𝕜 :=
    (↑f : E →ₗ[𝕜] 𝕜) ∘ₗ (↑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : WeakSpace 𝕜 E →ₗ[𝕜] E);
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' :
  u <
    (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ)
      ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
⊢ Continuous (Y := ℝ) fun (y : WeakSpace 𝕜 E) ↦ u

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx :
  Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' closure s)ᶜ
    ((LinearEquiv.toEquiv (toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) a : 𝕜) < u
hux : u < (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜)
f' : StrongDual.{u_1, u_2} 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (WeakSpace 𝕜 E) 𝕜 :=
    (↑f : E →ₗ[𝕜] 𝕜) ∘ₗ (↑(LinearEquiv.symm (toWeakSpace 𝕜 E)) : WeakSpace 𝕜 E →ₗ[𝕜] E);
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' :
  u <
    (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ)
      ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) x : WeakSpace 𝕜 E)
refine :
  Subset (α := Set (WeakSpace 𝕜 E)) ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s)
    {y : WeakSpace 𝕜 E | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ) y ≤ u}
⊢ Subset (α := Set (WeakSpace 𝕜 E)) (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))
    {y : WeakSpace 𝕜 E | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ) y ≤ u}

Tactic:
refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)

Premises used: closure_minimal, isClosed_le