awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (σ_li : (a : 𝕜₂) → 𝕜₃)
      ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
        𝕜₂)
have apply : Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
  (σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃)
Tactic: apply σ_li.continuous.comp
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
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 * x_1
have simp_rw : Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x.comp x_1
Tactic: simp_rw [mul_eq_comp]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
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 * x
have simp_rw : Continuous[instTopologicalSpace, instTopologicalSpace] fun (x_1 : F →WOT[𝕜₂] F) ↦ x_1.comp x
Tactic: simp_rw [mul_eq_comp]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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))
have 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
Tactic: refine le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
    (Set.compl_subset_compl.mp fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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
⊢ Membership.mem (γ := Set (WeakSpace 𝕜 E)) (closure ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))ᶜ x
have 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)
Tactic: obtain ⟨x, -, rfl⟩ := (toWeakSpace 𝕜 E).toEquiv.image_compl (closure s) |>.symm.subset hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (hypothesis)
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)
⊢ 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)
have this : ContinuousSMul ℝ E
Tactic: have : ContinuousSMul ℝ E := IsScalarTower.continuousSMul 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨f, u, hus, hux⟩ := RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜)
    hs.closure isClosed_closure (by simpa using hx)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (hypothesis)
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 := ⋯ }
⊢ 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)
have hux' : 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']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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}
have 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}
Tactic: refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (hypothesis)
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)
⊢ 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)
have 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}
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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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) ((closedConvexHull 𝕜 : (a : Set E) → Set E) s))
    ((closedConvexHull 𝕜 : (a : Set (WeakSpace 𝕜 E)) → Set (WeakSpace 𝕜 E))
      ((⇑(toWeakSpace 𝕜 E) : (a : E) → WeakSpace 𝕜 E) '' s))
have 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)))
Tactic: rw [closedConvexHull_eq_closure_convexHull (𝕜 := 𝕜),
    ((convex_convexHull 𝕜 s).lift ℝ).toWeakSpace_closure _, closedConvexHull_eq_closure_convexHull]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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))
    (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)))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (hypothesis)
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))
⊢ Subset.{u_3} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have h_convex : Convex.{0, u_3} ℝ (E := F) ((⇑e : (a : E) → F) '' s)
Tactic: have h_convex : Convex ℝ (e '' s) := hs.linear_image (F := F) e
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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.{u_3} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have 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)))
Tactic: rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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) → 𝕜)
⊢ Subset.{u_3} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have 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))
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)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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 := 𝕜)
    (AddHom.toFun
      (toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜)
        ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))))
have 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) → 𝕜)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakSpace (goal)
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))
have refine : LE.le.{u_3} (α := Set F) (closure ((⇑e : (a : E) → F) '' s)) ((⇑e : (a : E) → F) '' closure s)
Tactic: refine le_antisymm ((e : E →ₗ[𝕜] F).image_closure_of_convex hs he₁) ?_