awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) → 𝕜)
⊢ LE.le.{u_3} (α := Set F) (closure ((⇑e : (a : E) → F) '' s)) ((⇑e : (a : E) → F) '' closure s)
have 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))
Tactic: simp only [Set.le_eq_subset, ← Set.image_subset_image_iff e.symm.injective]
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := E →ₗ[𝕜] 𝕜) (↑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f) : E →ₗ[𝕜] 𝕜)
      ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))
f : StrongDual 𝕜 E
⊢ Eq (α := F →ₗ[𝕜] 𝕜) (↑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f) : F →ₗ[𝕜] 𝕜)
    ((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜))
have simp : ∀
  (he :
    ∀ (f : StrongDual 𝕜 F),
      Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
        (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)),
  Eq (α := (a : F) → 𝕜) (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜)
    (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
Tactic: simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢
Cleared hypotheses: he
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
g : StrongDual 𝕜 E
⊢ Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
    (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F)
      (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g : StrongDual 𝕜 F) : (a : F) → 𝕜) (⇑e : (a : E) → F))
have this : Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
  (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E)
          (↑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g) : F →ₗ[𝕜] 𝕜) :
        Module.Dual 𝕜 E) :
    (a : E) → 𝕜)
Tactic: have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
⊢ Eq (α := (a : F) → 𝕜) (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜)
    (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
have this : ∀ (g : StrongDual 𝕜 E),
  Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
    (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F)
      (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g : StrongDual 𝕜 F) : (a : F) → 𝕜) (⇑e : (a : E) → F))
Tactic: have (g : StrongDual 𝕜 E) : ⇑g = e_dual.symm g ∘ e := by
      have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
      simpa
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
this :
  ∀ (g : StrongDual 𝕜 E),
    Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
      (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F)
        (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g : StrongDual 𝕜 F) : (a : F) → 𝕜) (⇑e : (a : E) → F))
⊢ Eq (α := (a : F) → 𝕜) (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜)
    (⇑((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜)
have h : ∀ (x : F),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜) x : 𝕜)
    ((((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜) x :
      𝕜)
Tactic: ext x
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
this :
  ∀ (g : StrongDual 𝕜 E),
    Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
      (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F)
        (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g : StrongDual 𝕜 F) : (a : F) → 𝕜) (⇑e : (a : E) → F))
x : F
| ((((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜) x :
    𝕜)
have rw : Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (α := E) (β := F)
  (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜)
  ((⇑e : (a : E) → F) : (a : E) → F) ((e.symm : (a : F) → E) x : E)
Tactic: rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := (a : E) → 𝕜) (⇑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f : StrongDual 𝕜 E) : (a : E) → 𝕜)
      (⇑((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 E) : (a : E) → 𝕜)
this :
  ∀ (g : StrongDual 𝕜 E),
    Eq (α := (a : E) → 𝕜) (⇑g : (a : E) → 𝕜)
      (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F)
        (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) g : StrongDual 𝕜 F) : (a : F) → 𝕜) (⇑e : (a : E) → F))
x : F
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜) x : 𝕜)
    ((((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜) x :
      𝕜)
have h : Eq.{u_1 + 1} (α := 𝕜) ((((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜) x : 𝕜)
  (Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (α := E) (β := F)
      (⇑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f : StrongDual 𝕜 F) : (a : F) → 𝕜)
      ((⇑e : (a : E) → F) : (a : E) → F) ((e.symm : (a : F) → E) x : E) :
    𝕜)
Tactic: conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := E →ₗ[𝕜] 𝕜) (↑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f) : E →ₗ[𝕜] 𝕜)
      ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have he' : ∀ (f : StrongDual 𝕜 E),
  Eq (α := F →ₗ[𝕜] 𝕜) (↑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f) : F →ₗ[𝕜] 𝕜)
    ((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜))
Tactic: have he' (f : StrongDual 𝕜 E) : (e_dual.symm f : F →ₗ[𝕜] 𝕜) = e.symm.dualMap f := by
    simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢
    have (g : StrongDual 𝕜 E) : ⇑g = e_dual.symm g ∘ e := by
      have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
      simpa
    ext x
    conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
    simp
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := E →ₗ[𝕜] 𝕜) (↑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f) : E →ₗ[𝕜] 𝕜)
      ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))
he' :
  ∀ (f : StrongDual 𝕜 E),
    Eq (α := F →ₗ[𝕜] 𝕜) (↑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f) : F →ₗ[𝕜] 𝕜)
      ((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜))
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have refine_1 : ∀ (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) → 𝕜)
Tactic: refine e.image_closure_of_convex hs ?_ ?_
-- 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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he :
  ∀ (f : StrongDual 𝕜 F),
    Eq (α := E →ₗ[𝕜] 𝕜) (↑((e_dual : (a : StrongDual 𝕜 F) → StrongDual 𝕜 E) f) : E →ₗ[𝕜] 𝕜)
      ((e.dualMap : (a : Module.Dual 𝕜 F) → Module.Dual 𝕜 E) (↑f : F →ₗ[𝕜] 𝕜))
he' :
  ∀ (f : StrongDual 𝕜 E),
    Eq (α := F →ₗ[𝕜] 𝕜) (↑((e_dual.symm : (a : StrongDual 𝕜 E) → StrongDual 𝕜 F) f) : F →ₗ[𝕜] 𝕜)
      ((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜))
refine_1 :
  ∀ (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) → 𝕜)
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))
have refine_2 : ∀ (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) → 𝕜)
Tactic: refine e.image_closure_of_convex hs ?_ ?_
-- 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
R : Type u_4
V : Type u_5
inst_17 : CommRing R
inst_18 : TopologicalSpace R
inst_19 : T2Space R
inst_20 : ContinuousAdd R
inst_21 : ContinuousConstSMul R R
inst_22 : AddCommGroup V
inst_23 : Module R V
inst_24 : TopologicalSpace V
inst_25 : SeparatingDual R V
x x_1 : V
h :
  Eq (α := (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x : (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x_1 : (V →L[R] R) →ₗ[R] R)
⊢ x = x_1
have by_contra : ∀ (hne : ¬x = x_1), False
Tactic: by_contra hne
-- 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
R : Type u_4
V : Type u_5
inst_17 : CommRing R
inst_18 : TopologicalSpace R
inst_19 : T2Space R
inst_20 : ContinuousAdd R
inst_21 : ContinuousConstSMul R R
inst_22 : AddCommGroup V
inst_23 : Module R V
inst_24 : TopologicalSpace V
inst_25 : SeparatingDual R V
x x_1 : V
h :
  Eq (α := (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x : (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x_1 : (V →L[R] R) →ₗ[R] R)
hne : ¬x = x_1
⊢ False
have obtain : ∀ (f : StrongDual R V) (hf : Ne.{u_4 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) x_1 : R)), False
Tactic: obtain ⟨f, hf⟩ := SeparatingDual.exists_separating_of_ne (R := R) hne
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
i : ι
r : ℝ
hr : 0 < r
⊢ (p i).ball 0 r = (Finset.sup {i} p).ball 0 r
have rw : (p i).ball 0 r = (p i).ball 0 r
Tactic: rw [Finset.sup_singleton]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
⊢ univ = (Finset.sup ∅ p).ball 0 1
have rw : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) ⊥ 0 1)
Tactic: rw [Finset.sup_empty, Seminorm.bot_eq_zero, ball_zero' _ one_pos]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
rw : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) ⊥ 0 1)
⊢ univ = (Finset.sup ∅ p).ball 0 1
have rw₁ : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) 0 0 1)
Tactic: rw [Finset.sup_empty, Seminorm.bot_eq_zero, ball_zero' _ one_pos]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
rw : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) ⊥ 0 1)
rw₁ : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) 0 0 1)
⊢ univ = (Finset.sup ∅ p).ball 0 1
have rw₂ : Eq.{u_6 + 1} (α := Set E) univ univ
Tactic: rw [Finset.sup_empty, Seminorm.bot_eq_zero, ball_zero' _ one_pos]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU_1 : U ∈ p.basisSets
hV : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have rcases : ∀ (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂) (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
Tactic: rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have h : ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
Tactic: use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
have h : ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
Tactic: refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
have h : Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
  ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)
Tactic: rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
have rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
Tactic: classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)