awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) → 𝕜)
⊢ 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:
simpa [Set.image_image]
    using (e.symm : F →ₗ[𝕜] E).image_closure_of_convex (hs.linear_image (e : E →ₗ[𝕜] F)) he₂

Premises used: Set.image_image, LinearEquiv.symm, LinearMap.image_closure_of_convex, Convex.linear_image, 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
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
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) → 𝕜)
⊢ 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:
simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢

Premises used: DFunLike.ext'_iff, ContinuousLinearMap.coe_coe
-- 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
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) → 𝕜)
    (⇑((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
-- 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
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
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) → 𝕜)
⊢ 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:
simpa
-- 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
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))

Tactic:
have (g : StrongDual 𝕜 E) : ⇑g = e_dual.symm g ∘ e := by
      have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
      simpa
-- 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
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))
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 :
        𝕜)
⊢ 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:
ext x
-- 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
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
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)
| ((((e.symm.dualMap : (a : Module.Dual 𝕜 E) → Module.Dual 𝕜 F) (↑f : E →ₗ[𝕜] 𝕜) : Module.Dual 𝕜 F) : (a : F) → 𝕜) x :
    𝕜)

Tactic:
rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]

Premises used: ContinuousLinearMap.coe_coe, LinearEquiv.dualMap_apply
-- 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
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
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) :
      𝕜)
⊢ 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:
conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]

Premises used: ContinuousLinearMap.coe_coe, LinearEquiv.dualMap_apply
-- 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
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 : 𝕜)
    (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:
simp
-- 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
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 →ₗ[𝕜] 𝕜))

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
-- 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
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))

Tactic:
e.image_closure_of_convex hs ?_ ?_

Premises used: LinearEquiv.image_closure_of_convex
-- 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
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) → 𝕜)
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) → 𝕜)
⊢ Eq.{u_3 + 1} (α := Set F) ((⇑e : (a : E) → F) '' closure s) (closure ((⇑e : (a : E) → F) '' s))

Tactic:
refine e.image_closure_of_convex hs ?_ ?_

Premises used: LinearEquiv.image_closure_of_convex
-- 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
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 →ₗ[𝕜] 𝕜))
⊢ ∀ (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:
simpa [← he] using fun f ↦ map_continuous (e_dual f)

Premises used: ContinuousMapClass.map_continuous, DFunLike.coe
-- 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
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 →ₗ[𝕜] 𝕜))
⊢ ∀ (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:
simpa [← he'] using fun f ↦ map_continuous (e_dual.symm f)

Premises used: ContinuousMapClass.map_continuous, Equiv.symm, DFunLike.coe
-- 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
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)
by_contra : ∀ (hne : ¬x = x_1), False
⊢ x = x_1

Tactic:
by_contra hne
-- 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
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
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
⊢ False

Tactic:
obtain ⟨f, hf⟩ := SeparatingDual.exists_separating_of_ne (R := R) hne

Premises used: SeparatingDual.exists_separating_of_ne