awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i : (a : WeakDual 𝕜 E) → ℝ) x < r
C : ℝ
hC :
  ∀ (i : (↑s : Type (max u_1 u_3))),
    norm (E := E →L[𝕜] 𝕜) ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) (↑i : WeakDual 𝕜 E) : StrongDual 𝕜 E) ≤
      C
⊢ ∃ (C : ℝ),
    ∀ (x : StrongDual 𝕜 E),
      Membership.mem (γ := Set (StrongDual 𝕜 E)) ((⇑StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) ⁻¹' s)
          x →
        ‖x‖ ≤ C

Tactic:
⟨C, fun f hf ↦ hC ⟨StrongDual.toWeakDual f, hf⟩⟩

Premises used: StrongDual.toWeakDual, Subtype.mk, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i : (a : WeakDual 𝕜 E) → ℝ) x < r
C : ℝ
hC :
  ∀ (i : (↑s : Type (max u_1 u_3))),
    norm (E := E →L[𝕜] 𝕜) ((toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) (↑i : WeakDual 𝕜 E) : StrongDual 𝕜 E) ≤
      C
⊢ ∃ (C : ℝ),
    ∀ (x : StrongDual 𝕜 E),
      Membership.mem (γ := Set (StrongDual 𝕜 E)) ((⇑StrongDual.toWeakDual : (a : StrongDual 𝕜 E) → WeakDual 𝕜 E) ⁻¹' s)
          x →
        ‖x‖ ≤ C

Tactic:
exact ⟨C, fun f hf ↦ hC ⟨StrongDual.toWeakDual f, hf⟩⟩
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ IsClosed[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E) ↦ 𝕜) '' s)

Tactic:
ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed hb (isClosed_induced_iff'.1 hc)

Premises used: ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed, isClosed_induced_iff', WeakBilin, WeakDual, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ IsCompact s

Tactic:
DFunLike.coe_injective.isEmbedding_induced.isCompact_iff.mpr <|
    ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image hb <|
      isClosed_image_coe_of_bounded_of_closed hb hc

Premises used: Iff.mpr, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image, Topology.IsEmbedding.isCompact_iff, WeakDual, DFunLike.coe_injective, Function.Injective.isEmbedding_induced, WeakDual.isClosed_image_coe_of_bounded_of_closed
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x' : StrongDual 𝕜 E
r : ℝ
⊢ IsClosed (X := WeakDual 𝕜 E) ((⇑toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) ⁻¹' closedBall x' r)

Tactic:
isClosed_induced_iff'.2 (ContinuousLinearMap.is_weak_closed_closedBall x' r)

Premises used: Iff.mpr, isClosed_induced_iff', WeakDual, ContinuousLinearMap.is_weak_closed_closedBall
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x' : StrongDual 𝕜 E
r : ℝ
⊢ Bornology.IsBounded (α := WeakDual 𝕜 E) ((⇑toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) ⁻¹' closedBall x' r)

Tactic:
isBounded_toStrongDual_preimage_iff_isBounded.mpr Metric.isBounded_closedBall

Premises used: Iff.mpr, Metric.isBounded_closedBall, WeakDual.isBounded_toStrongDual_preimage_iff_isBounded
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
obtain : ∀ (R : ℝ) (hR : s ⊆ closedBall 0 R), Bornology.IsBounded (closure s)
⊢ Bornology.IsBounded (closure s)

Tactic:
obtain ⟨R, hR⟩ := (Metric.isBounded_iff_subset_closedBall (0 : StrongDual 𝕜 E)).mp hb

Premises used: Iff.mp, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
R : ℝ
hR : s ⊆ closedBall 0 R
⊢ Bornology.IsBounded (closure s)

Tactic:
(isBounded_closedBall 0 R).subset
    (closure_minimal (fun y hy ↦ hR (a := toStrongDual y) hy) (isClosed_closedBall 0 R))

Premises used: closure_minimal, WeakDual.isClosed_closedBall, Bornology.IsBounded.subset, WeakDual.isBounded_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
R : ℝ
hR : s ⊆ closedBall 0 R
⊢ Bornology.IsBounded (closure s)

Tactic:
exact (isBounded_closedBall 0 R).subset
    (closure_minimal (fun y hy ↦ hR (a := toStrongDual y) hy) (isClosed_closedBall 0 R))

Premises used: closure_minimal, WeakDual.isClosed_closedBall, Bornology.IsBounded.subset, WeakDual.isBounded_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace 𝕜
x' : StrongDual 𝕜 E
r : ℝ
⊢ IsCompact (X := WeakDual 𝕜 E) ((⇑toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) ⁻¹' closedBall x' r)

Tactic:
isCompact_of_bounded_of_closed (isBounded_closedBall x' r) (isClosed_closedBall x' r)

Premises used: WeakDual.isClosed_closedBall, WeakDual.isCompact_of_bounded_of_closed, WeakDual.isBounded_closedBall
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
M : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : Module 𝕜 M
s : Set M
⊢ Eq (α := Set (WeakDual 𝕜 M)) (polar 𝕜 s)
    {f : WeakDual 𝕜 M | ∀ x ∈ s, norm.{u_1} (E := 𝕜) ((f : (a : M) → 𝕜) x : 𝕜) ≤ 1}

Tactic:
rfl

Premises used: WeakDual.polar, Set.Mem, setOf, StrongDual.polar, LinearMap.polar, Set.preimage, rfl
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
M : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : Module 𝕜 M
s : Set M
simp : IsClosed (X := WeakDual 𝕜 M) (⋂ i ∈ s, {x : WeakDual 𝕜 M | norm.{u_1} (E := 𝕜) ((x : (a : M) → 𝕜) i : 𝕜) ≤ 1})
⊢ IsClosed (X := WeakDual 𝕜 M) (polar 𝕜 s)

Tactic:
simp only [polar_def, setOf_forall]

Premises used: WeakDual.polar_def, Set.setOf_forall
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
M : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : Module 𝕜 M
s : Set M
⊢ IsClosed (X := WeakDual 𝕜 M) (⋂ i ∈ s, {x : WeakDual 𝕜 M | norm.{u_1} (E := 𝕜) ((x : (a : M) → 𝕜) i : 𝕜) ≤ 1})

Tactic:
isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm

Premises used: isClosed_biInter, Continuous.norm, isClosed_Iic, topDualPairing, WeakBilin.eval_continuous, IsClosed.preimage
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
M : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : Module 𝕜 M
s : Set M
⊢ IsClosed (X := WeakDual 𝕜 M) (⋂ i ∈ s, {x : WeakDual 𝕜 M | norm.{u_1} (E := 𝕜) ((x : (a : M) → 𝕜) i : 𝕜) ≤ 1})

Tactic:
exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm

Premises used: isClosed_biInter, Continuous.norm, isClosed_Iic, WeakBilin.eval_continuous, IsClosed.preimage
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Bornology.IsBounded (α := WeakDual 𝕜 E) (polar 𝕜 s)

Tactic:
isBounded_toStrongDual_preimage_iff_isBounded.mpr
  (NormedSpace.isBounded_polar_of_mem_nhds_zero 𝕜 s_nhds)

Premises used: NormedSpace.isBounded_polar_of_mem_nhds_zero, Iff.mpr, WeakDual.polar, WeakDual.isBounded_toStrongDual_preimage_iff_isBounded
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ IsClosed[Pi.topologicalSpace] (image (α := WeakDual 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ 𝕜)) (polar 𝕜 s))

Tactic:
isClosed_image_coe_of_bounded_of_closed (isBounded_polar 𝕜 s_nhds) (isClosed_polar _ _)

Premises used: WeakDual.isClosed_polar, WeakDual.isBounded_polar, WeakDual.isClosed_image_coe_of_bounded_of_closed
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ IsClosed[Pi.topologicalSpace]
    (image (α := StrongDual 𝕜 E) (DFunLike.coe (β := fun (x : E) ↦ 𝕜) : StrongDual 𝕜 E → (a : E) → 𝕜)
      (StrongDual.polar 𝕜 s : Set (StrongDual 𝕜 E)))

Tactic:
WeakDual.isClosed_image_polar_of_mem_nhds 𝕜 s_nhds

Premises used: WeakDual.isClosed_image_polar_of_mem_nhds, WeakDual.polar, Set.Mem, setOf, StrongDual.polar, LinearMap.polar, WeakBilin, Set.preimage, WeakDual
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace 𝕜
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ IsCompact (X := WeakDual 𝕜 E) (polar 𝕜 s)

Tactic:
isCompact_of_bounded_of_closed (isBounded_polar 𝕜 s_nhds) (isClosed_polar _ _)

Premises used: WeakDual.isClosed_polar, WeakDual.isBounded_polar, WeakDual.isCompact_of_bounded_of_closed
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
h :
  (∀ (n : ℕ),
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n)) ∧
    ∀ ⦃x y : WeakDual 𝕜 E⦄,
      x ≠ y →
        ∃ (n : ℕ),
          Ne.{u_1 + 1} (α := 𝕜) ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n x)
            ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n y)
⊢ ∃ (gs : ℕ → WeakDual 𝕜 E → 𝕜),
    (∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n)) ∧
      ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y

Tactic:
use (fun n φ ↦ φ (denseSeq E n))
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
h :
  ∀ (n : ℕ),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (φ : WeakDual 𝕜 E) ↦
      (φ : (a : E) → 𝕜) (denseSeq E n)
h₁ :
  ∀ ⦃x y : WeakDual 𝕜 E⦄,
    x ≠ y →
      ∃ (n : ℕ), Ne.{u_1 + 1} (α := 𝕜) ((x : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)
⊢ (∀ (n : ℕ),
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n)) ∧
    ∀ ⦃x y : WeakDual 𝕜 E⦄,
      x ≠ y →
        ∃ (n : ℕ),
          Ne.{u_1 + 1} (α := 𝕜) ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n x)
            ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n y)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
⊢ ∀ (n : ℕ),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (φ : WeakDual 𝕜 E) ↦
      (φ : (a : E) → 𝕜) (denseSeq E n)

Tactic:
fun _ ↦ eval_continuous _

Premises used: TopologicalSpace.denseSeq, WeakDual.eval_continuous
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
⊢ ∀ (n : ℕ),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (φ : WeakDual 𝕜 E) ↦
      (φ : (a : E) → 𝕜) (denseSeq E n)

Tactic:
exact fun _ ↦ eval_continuous _

Premises used: WeakDual.eval_continuous
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
w y : WeakDual 𝕜 E
w_ne_y : w ≠ y
h :
  ∀
    (w_ne_y :
      ∀ (n : ℕ), Eq.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)),
    w = y
⊢ ∃ (n : ℕ), Ne.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)

Tactic:
contrapose! w_ne_y
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
w y : WeakDual 𝕜 E
w_ne_y : ∀ (n : ℕ), Eq.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)
⊢ w = y

Tactic:
DFunLike.ext'_iff.mpr <| (map_continuous w).ext_on
      (denseRange_denseSeq E) (map_continuous y) (Set.eqOn_range.mpr (funext w_ne_y))

Premises used: Iff.mpr, TopologicalSpace.denseRange_denseSeq, DFunLike.ext'_iff, Set.eqOn_range, funext, Continuous.ext_on, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
w y : WeakDual 𝕜 E
w_ne_y : ∀ (n : ℕ), Eq.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)
⊢ w = y

Tactic:
exact DFunLike.ext'_iff.mpr <| (map_continuous w).ext_on
      (denseRange_denseSeq E) (map_continuous y) (Set.eqOn_range.mpr (funext w_ne_y))

Premises used: Iff.mpr, TopologicalSpace.denseRange_denseSeq, DFunLike.ext'_iff, Set.eqOn_range, funext, Continuous.ext_on, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
⊢ CompactSpace (↑K : Type (max u_1 u_3))

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp K_cpt
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
this : CompactSpace (↑K : Type (max u_1 u_3))
obtain :
  ∀ (gs : ℕ → WeakDual 𝕜 E → 𝕜)
    (gs_cont : ∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n))
    (gs_sep : ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y), MetrizableSpace (↑K : Type (max u_1 u_3))
⊢ MetrizableSpace (↑K : Type (max u_1 u_3))

Tactic:
obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 E

Premises used: WeakDual.exists_countable_separating
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
this : CompactSpace (↑K : Type (max u_1 u_3))
gs : ℕ → WeakDual 𝕜 E → 𝕜
gs_cont : ∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n)
gs_sep : ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y
⊢ MetrizableSpace (↑K : Type (max u_1 u_3))

Tactic:
Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating
    (fun n k ↦ gs n k) (fun n ↦ (gs_cont n).comp continuous_subtype_val)
    fun x y hxy ↦ gs_sep <| Subtype.val_injective.ne hxy

Premises used: Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating, continuous_subtype_val, Subtype.val_injective, Continuous.comp, Function.Injective.ne, Subtype.val
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
this : CompactSpace (↑K : Type (max u_1 u_3))
gs : ℕ → WeakDual 𝕜 E → 𝕜
gs_cont : ∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n)
gs_sep : ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y
⊢ MetrizableSpace (↑K : Type (max u_1 u_3))

Tactic:
exact Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating
    (fun n k ↦ gs n k) (fun n ↦ (gs_cont n).comp continuous_subtype_val)
    fun x y hxy ↦ gs_sep <| Subtype.val_injective.ne hxy
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ CompactSpace (↑s : Type (max u_1 u_3))

Tactic:
have b_isCompact' : CompactSpace s :=
    isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
⊢ MetrizableSpace (↑s : Type (max u_1 u_3))

Tactic:
have b_isMetrizable : TopologicalSpace.MetrizableSpace s :=
    metrizable_of_isCompact 𝕜 E s <| isCompact_of_bounded_of_closed hb hc
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
b_isMetrizable : MetrizableSpace (↑s : Type (max u_1 u_3))
⊢ SeqContinuous (Y := WeakDual 𝕜 E) fun (φ : (↑s : Type (max u_1 u_3))) ↦ (↑φ : WeakDual 𝕜 E)

Tactic:
have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 E)) :=
    continuous_iff_seqContinuous.mp continuous_subtype_val
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
b_isMetrizable : MetrizableSpace (↑s : Type (max u_1 u_3))
seq_cont_phi : SeqContinuous (Y := WeakDual 𝕜 E) fun (φ : (↑s : Type (max u_1 u_3))) ↦ (↑φ : WeakDual 𝕜 E)
⊢ IsSeqCompact s

Tactic:
simpa using IsSeqCompact.range seq_cont_phi

Premises used: IsSeqCompact.range
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set E
s_nhd : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ IsSeqCompact (X := WeakDual 𝕜 E) (polar 𝕜 s)

Tactic:
isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)

Premises used: WeakDual.isClosed_polar, WeakDual.isBounded_polar, WeakDual.isSeqCompact_of_isBounded_of_isClosed
-- Module: Mathlib.Analysis.Normed.Module.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
x' : StrongDual 𝕜 E
r : ℝ
⊢ IsSeqCompact (X := WeakDual 𝕜 E) ((⇑toStrongDual : (a : WeakDual 𝕜 E) → StrongDual 𝕜 E) ⁻¹' closedBall x' r)

Tactic:
isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_closedBall x' r) (isClosed_closedBall x' r)

Premises used: WeakDual.isClosed_closedBall, WeakDual.isBounded_closedBall, WeakDual.isSeqCompact_of_isBounded_of_isClosed
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simpa [smul_zero] using dist_smul_pair r 0 x

Premises used: smul_zero, OfNat.ofNat, dist_smul_pair
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊

Tactic:
norm_smul_le _ _

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_mul] using nnnorm_smul_le ..

Premises used: ENNReal.coe_mul, ENorm.enorm, nnnorm_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Tactic:
simpa only [dist_eq_norm_neg_add, add_zero, norm_neg] using dist_smul_pair s x y

Premises used: dist_eq_norm_neg_add, norm_neg, add_zero, dist_smul_pair
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
s : α
x y : β
⊢ nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y

Tactic:
dist_smul_le s x y

Premises used: dist_smul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
s : α
⊢ LipschitzWith (β := β) ‖s‖₊ fun (x : β) ↦ s • x

Tactic:
lipschitzWith_iff_dist_le_mul.2 <| dist_smul_le _

Premises used: Iff.mpr, dist_smul_le, lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedAddGroup α
inst_1 : SeminormedAddGroup β
inst_2 : SMulZeroClass α β
inst_3 : IsBoundedSMul α β
s : α
x y : β
⊢ edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y

Tactic:
lipschitzWith_smul s x y

Premises used: lipschitzWith_smul
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)

Premises used: dist_eq_norm, mul_sub, HSub.hSub, norm_mul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSeminormedRing α
x₁ x₂ y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
simpa [sub_mul, dist_eq_norm] using norm_mul_le (x₁ - x₂) y

Premises used: dist_eq_norm, HSub.hSub, sub_mul, norm_mul_le
-- Module: Mathlib.Analysis.Normed.MulAction
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSeminormedRing α
x : αᵐᵒᵖ
y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop

Premises used: dist_eq_norm, HSub.hSub, sub_mul, mul_comm, MulOpposite.unop, norm_mul_le