awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
y : E
hy : y ∈ s
⊢ Membership.mem (α := WeakSpace 𝕜 E) (γ := Set (WeakSpace 𝕜 E))
    {y : WeakSpace 𝕜 E | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f' : (a : WeakSpace 𝕜 E) → ℝ) y ≤ u}
    ((toWeakSpace 𝕜 E : (a : E) → WeakSpace 𝕜 E) y : WeakSpace 𝕜 E)

Tactic:
simpa [f'] using (hus y <| subset_closure hy).le

Premises used: subset_closure, LT.lt.le
-- 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)
⊢ 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:
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
-- 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)
hus' :
  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}
⊢ 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:
(hux'.not_ge <| hus' ·)

Premises used: Set.Mem, setOf, LT.lt.not_ge, Not
-- 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)
hus' :
  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}
⊢ 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:
exact (hux'.not_ge <| hus' ·)

Premises used: LT.lt.not_ge
-- 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
rw :
  Eq (α := Set (WeakSpace 𝕜 E))
    (closure
      (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((convexHull 𝕜 : (a : Set E) → Set E) s)))
    (closure
      ((convexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
        ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s)))
⊢ Eq (α := Set (WeakSpace 𝕜 E))
    (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((closedConvexHull 𝕜 : (a : Set E) → Set E) s))
    ((closedConvexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
      ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))

Tactic:
rw [closedConvexHull_eq_closure_convexHull (𝕜 := 𝕜),
    ((convex_convexHull 𝕜 s).lift ℝ).toWeakSpace_closure _, closedConvexHull_eq_closure_convexHull]

Premises used: Real, closedConvexHull_eq_closure_convexHull, Convex.toWeakSpace_closure, convex_convexHull, Convex.lift
-- 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
e_s :
  Eq (α := Set (WeakSpace 𝕜 E))
    (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
      ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))
⊢ Eq (α := Set (WeakSpace 𝕜 E))
    (closure
      (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((convexHull 𝕜 : (a : Set E) → Set E) s)))
    (closure
      ((convexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
        ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s)))

Tactic:
congr
-- 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
⊢ Eq (α := Set (WeakSpace 𝕜 E))
    (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
      ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))

Tactic:
LinearMap.image_convexHull (toWeakSpace 𝕜 E).toLinearMap s

Premises used: LinearEquiv.toLinearMap, LinearMap.image_convexHull, toWeakSpace
-- 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
⊢ Eq (α := Set (WeakSpace 𝕜 E))
    (Set.image (α := E) (⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
      ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))

Tactic:
refine LinearMap.image_convexHull (toWeakSpace 𝕜 E).toLinearMap s

Premises used: LinearEquiv.toLinearMap, LinearMap.image_convexHull, toWeakSpace
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he' :
  Continuous.{u_2, u_3} (Y := WeakSpace 𝕜 F) fun (x : WeakSpace 𝕜 E) ↦
    (toWeakSpace 𝕜 F : (a : F) → WeakSpace 𝕜 F)
      ((e : (a : E) → F) ((LinearEquiv.symm (toWeakSpace 𝕜 E) : (a : WeakSpace 𝕜 E) → E) x : E))
⊢ Convex.{0, u_3} ℝ (E := F) ((⇑e : (a : E) → F) '' s)

Tactic:
have h_convex : Convex ℝ (e '' s) := hs.linear_image (F := F) e
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he' :
  Continuous.{u_2, u_3} (Y := WeakSpace 𝕜 F) fun (x : WeakSpace 𝕜 E) ↦
    (toWeakSpace 𝕜 F : (a : F) → WeakSpace 𝕜 F)
      ((e : (a : E) → F) ((LinearEquiv.symm (toWeakSpace 𝕜 E) : (a : WeakSpace 𝕜 E) → E) x : E))
h_convex : Convex.{0, u_3} ℝ (E := F) ((⇑e : (a : E) → F) '' s)
rw :
  Subset (α := Set (WeakSpace 𝕜 F))
    (Set.image (α := F) (⇑(toWeakSpace 𝕜 F) : (a : F) → WeakSpace 𝕜 F) ((⇑e : (a : E) → F) '' closure s))
    (closure (Set.image (α := F) (⇑(toWeakSpace 𝕜 F) : (a : F) → WeakSpace 𝕜 F) ((⇑e : (a : E) → F) '' s)))
⊢ Subset.{u_3} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))

Tactic:
rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]

Premises used: Convex.toWeakSpace_closure, Set.image_subset_image_iff, toWeakSpace, LinearEquiv.injective
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he' :
  Continuous.{u_2, u_3} (Y := WeakSpace 𝕜 F) fun (x : WeakSpace 𝕜 E) ↦
    (toWeakSpace 𝕜 F : (a : F) → WeakSpace 𝕜 F)
      ((e : (a : E) → F) ((LinearEquiv.symm (toWeakSpace 𝕜 E) : (a : WeakSpace 𝕜 E) → E) x : E))
h_convex : Convex.{0, u_3} ℝ (E := F) ((⇑e : (a : E) → F) '' s)
⊢ Subset (α := Set (WeakSpace 𝕜 F))
    (Set.image (α := F) (⇑(toWeakSpace 𝕜 F) : (a : F) → WeakSpace 𝕜 F) ((⇑e : (a : E) → F) '' closure s))
    (closure (Set.image (α := F) (⇑(toWeakSpace 𝕜 F) : (a : F) → WeakSpace 𝕜 F) ((⇑e : (a : E) → F) '' s)))

Tactic:
simpa only [Set.image_image, ← hs.toWeakSpace_closure 𝕜, LinearEquiv.symm_apply_apply]
      using he'.continuousOn.image_closure (s := toWeakSpace 𝕜 E '' s)

Premises used: Set.image_image, Continuous.continuousOn, Convex.toWeakSpace_closure, LinearEquiv.symm_apply_apply, ContinuousOn.image_closure
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
suffices :
  Continuous.{u_2, u_3} (Y := WeakSpace 𝕜 F) fun (x : WeakSpace 𝕜 E) ↦
    (toWeakSpace 𝕜 F : (a : F) → WeakSpace 𝕜 F)
      ((e : (a : E) → F) ((LinearEquiv.symm (toWeakSpace 𝕜 E) : (a : WeakSpace 𝕜 E) → E) x : E))
⊢ Subset.{u_3} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))

Tactic:
suffices he' : Continuous (toWeakSpace 𝕜 F <| e <| (toWeakSpace 𝕜 E).symm ·) by
    have h_convex : Convex ℝ (e '' s) := hs.linear_image (F := F) e
    rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]
    simpa only [Set.image_image, ← hs.toWeakSpace_closure 𝕜, LinearEquiv.symm_apply_apply]
      using he'.continuousOn.image_closure (s := toWeakSpace 𝕜 E '' s)
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
f : F →L[𝕜] 𝕜
dsimp :
  Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
    (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
    (AddHom.toFun
      (toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
        ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))))

Tactic:
dsimp
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
f : F →L[𝕜] 𝕜
⊢ Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
    (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
⊢ Continuous.{u_2, u_3} (Y := WeakSpace 𝕜 F) fun (x : WeakSpace 𝕜 E) ↦
    (toWeakSpace 𝕜 F : (a : F) → WeakSpace 𝕜 F)
      ((e : (a : E) → F) ((LinearEquiv.symm (toWeakSpace 𝕜 E) : (a : WeakSpace 𝕜 E) → E) x : E))

Tactic:
exact WeakBilin.continuous_of_continuous_eval _ fun f ↦ WeakBilin.eval_continuous _ ({
      toLinearMap := e.dualMap f
      cont := by dsimp; fun_prop } : StrongDual 𝕜 E)

Premises used: WeakBilin.continuous_of_continuous_eval
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he₂ :
  ∀ (f : StrongDual 𝕜 E),
    Continuous.{u_3, u_1} (X := F) (Y := 𝕜)
      (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))

Tactic:
le_antisymm ((e : E →ₗ[𝕜] F).image_closure_of_convex hs he₁) ?_

Premises used: LinearMap.image_closure_of_convex, le_antisymm, LinearEquiv.toLinearMap
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he₂ :
  ∀ (f : StrongDual 𝕜 E),
    Continuous.{u_3, u_1} (X := F) (Y := 𝕜)
      (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
refine : LE.le.{u_3} (α := Set F) (closure ((⇑e : (a : E) → F) '' s)) ((⇑e : (a : E) → F) '' closure s)
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))

Tactic:
refine le_antisymm ((e : E →ₗ[𝕜] F).image_closure_of_convex hs he₁) ?_

Premises used: LinearMap.image_closure_of_convex, le_antisymm, LinearEquiv.toLinearMap
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ :
  ∀ (f : StrongDual 𝕜 F),
    Continuous.{u_2, u_1} (X := E) (Y := 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
he₂ :
  ∀ (f : StrongDual 𝕜 E),
    Continuous.{u_3, u_1} (X := F) (Y := 𝕜)
      (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
simp :
  Subset.{u_2} (α := Set E) (Set.image.{u_3, u_2} (α := F) (⇑e.symm : (a : F) → E) (closure ((⇑e : (a : E) → F) '' s)))
    (Set.image.{u_3, u_2} (α := F) (⇑e.symm : (a : F) → E) ((⇑e : (a : E) → F) '' closure s))
⊢ LE.le.{u_3} (α := Set F) (closure ((⇑e : (a : E) → F) '' s)) ((⇑e : (a : E) → F) '' closure s)

Tactic:
simp only [Set.le_eq_subset, ← Set.image_subset_image_iff e.symm.injective]

Premises used: LinearEquiv.symm, Set.le_eq_subset, Set.image_subset_image_iff, LinearEquiv.injective