awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
seg.mp <| .mono ?_ (fun _ => forall₂_imp)

Premises used: forall₂_imp, Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
refine : ∀ᶠ (x : α) in f, ∀ (a : E) (b : a ∈ [y x -[ℝ] z x]), a ∈ s → r x a
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
refine seg.mp <| .mono ?_ (fun _ => forall₂_imp)

Premises used: Filter.Eventually.mp
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
apply : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, p.2 ∈ s → r p.1 p.2
⊢ ∀ᶠ (x : α) in f, ∀ (a : E) (b : a ∈ [y x -[ℝ] z x]), a ∈ s → r x a

Tactic:
apply Eventually.segment_of_prod_nhds hy hz

Premises used: Filter.Eventually.segment_of_prod_nhds
-- Module: Mathlib.Analysis.Normed.Module.Convex
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
⊢ ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, p.2 ∈ s → r p.1 p.2

Tactic:
simpa [nhdsWithin, prod_eq_inf, ← inf_assoc, eventually_inf_principal] using hr

Premises used: Filter.eventually_inf_principal, nhdsWithin, Filter.prod_eq_inf, inf_assoc
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : StrongDual 𝕜 E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) :
          (a : StrongDual 𝕜 E) → 𝕜)
        f :
      𝕜)
    ((f : (a : E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ sorry = norm (E := StrongDual 𝕜 E →L[𝕜] StrongDual 𝕜 E) (ContinuousLinearMap.id 𝕜 (StrongDual 𝕜 E))

Tactic:
ContinuousLinearMap.opNorm_flip _

Premises used: ContinuousLinearMap.opNorm_flip
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
apply :
  ‖x‖ ≤
    norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))
⊢ norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((((↑(inclusionInDoubleDual 𝕜 E) : E →ₗ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)) :
              E →ₗ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)) :
            (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E))
          x :
        StrongDual 𝕜 (StrongDual 𝕜 E)) =
    ‖x‖

Tactic:
apply le_antisymm (double_dual_bound 𝕜 E x)

Premises used: le_antisymm, NormedSpace.double_dual_bound
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
obtain :
  ∀ (g : StrongDual 𝕜 E) (hg : ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)),
    ‖x‖ ≤
      norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
        ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))
⊢ ‖x‖ ≤
    norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))

Tactic:
obtain ⟨g, hg⟩ := exists_dual_vector'' 𝕜 x

Premises used: exists_dual_vector''
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
g : StrongDual 𝕜 E
hg : ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
grw :
  ‖x‖ ≤
    norm.{v} (E := 𝕜)
      ((((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) :
            (a : StrongDual 𝕜 E) → 𝕜)
          g :
        𝕜)
⊢ ‖x‖ ≤
    norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))

Tactic:
grw [← (inclusionInDoubleDual 𝕜 E x).unit_le_opNorm g hg.left]

Premises used: NormedSpace.inclusionInDoubleDual, And.left, ContinuousLinearMap.unit_le_opNorm, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
g : StrongDual 𝕜 E
hg : ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ‖x‖ ≤
    norm.{v} (E := 𝕜)
      ((((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) :
            (a : StrongDual 𝕜 E) → 𝕜)
          g :
        𝕜)

Tactic:
simp [hg.right]

Premises used: And.right
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), norm.{v} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ M * ‖f‖
rw :
  norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDualLi 𝕜 : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) ≤
    M
⊢ ‖x‖ ≤ M

Tactic:
rw [← (inclusionInDoubleDualLi (E := E) 𝕜).norm_map x]

Premises used: LinearIsometry.norm_map, NormedSpace.inclusionInDoubleDualLi
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), norm.{v} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ M * ‖f‖
⊢ norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDualLi 𝕜 : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) ≤
    M

Tactic:
ContinuousLinearMap.opNorm_le_bound _ hMp hM

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), norm.{v} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ M * ‖f‖
⊢ norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDualLi 𝕜 : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) ≤
    M

Tactic:
exact ContinuousLinearMap.opNorm_le_bound _ hMp hM

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : SeminormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
⊢ Eq (α := WeakSpace 𝕜 X →ₗ[𝕜] WeakDual 𝕜 (StrongDual 𝕜 X))
    (↑(inclusionInDoubleDualWeak 𝕜 X) : WeakSpace 𝕜 X →ₗ[𝕜] WeakDual 𝕜 (StrongDual 𝕜 X))
    ((LinearEquiv.arrowCongr (toWeakSpace 𝕜 X) StrongDual.toWeakDual :
        (a : X →ₗ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 X)) → WeakSpace 𝕜 X →ₗ[𝕜] WeakDual 𝕜 (StrongDual 𝕜 X))
      (↑(inclusionInDoubleDual 𝕜 X) : X →ₗ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
X : Type u_4
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (α := X) ((⇑(toWeakSpace 𝕜 X) : (a : X) → WeakSpace 𝕜 X) ⁻¹' S)
hrange :
  Subset (α := Set (WeakDual 𝕜 (StrongDual 𝕜 X)))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
    (Set.range (ι := WeakSpace 𝕜 X)
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)))
rw :
  IsCompact.{u_4} (X := WeakSpace 𝕜 X)
    (Set.preimage (β := WeakDual 𝕜 (StrongDual 𝕜 X))
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X))
      (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S)))
⊢ IsCompact (closure S)

Tactic:
rw [(isEmbedding_inclusionInDoubleDualWeak 𝕜 X).closure_eq_preimage_closure_image]

Premises used: NormedSpace.isEmbedding_inclusionInDoubleDualWeak, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
X : Type u_4
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (α := X) ((⇑(toWeakSpace 𝕜 X) : (a : X) → WeakSpace 𝕜 X) ⁻¹' S)
hrange :
  Subset (α := Set (WeakDual 𝕜 (StrongDual 𝕜 X)))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
    (Set.range (ι := WeakSpace 𝕜 X)
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)))
apply :
  IsCompact (X := WeakDual 𝕜 (StrongDual 𝕜 X))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
⊢ IsCompact.{u_4} (X := WeakSpace 𝕜 X)
    (Set.preimage (β := WeakDual 𝕜 (StrongDual 𝕜 X))
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X))
      (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S)))

Tactic:
apply (isEmbedding_inclusionInDoubleDualWeak 𝕜 X).isCompact_preimage' _ hrange

Premises used: NormedSpace.isEmbedding_inclusionInDoubleDualWeak, Topology.IsInducing.isCompact_preimage', Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
X : Type u_4
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (α := X) ((⇑(toWeakSpace 𝕜 X) : (a : X) → WeakSpace 𝕜 X) ⁻¹' S)
hrange :
  Subset (α := Set (WeakDual 𝕜 (StrongDual 𝕜 X)))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
    (Set.range (ι := WeakSpace 𝕜 X)
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)))
⊢ IsCompact (X := WeakDual 𝕜 (StrongDual 𝕜 X))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))

Tactic:
WeakDual.isCompact_of_bounded_of_closed

Premises used: WeakDual.isCompact_of_bounded_of_closed
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
X : Type u_4
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (α := X) ((⇑(toWeakSpace 𝕜 X) : (a : X) → WeakSpace 𝕜 X) ⁻¹' S)
hrange :
  Subset (α := Set (WeakDual 𝕜 (StrongDual 𝕜 X)))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
    (Set.range (ι := WeakSpace 𝕜 X)
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)))
⊢ IsBounded (α := WeakDual 𝕜 (StrongDual 𝕜 X))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))

Tactic:
WeakDual.isBounded_closure

Premises used: WeakDual.isBounded_closure
-- Module: Mathlib.Analysis.Normed.Module.DoubleDual
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
X : Type u_4
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (α := X) ((⇑(toWeakSpace 𝕜 X) : (a : X) → WeakSpace 𝕜 X) ⁻¹' S)
hrange :
  Subset (α := Set (WeakDual 𝕜 (StrongDual 𝕜 X)))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
    (Set.range (ι := WeakSpace 𝕜 X)
      (⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)))
⊢ IsCompact (X := WeakDual 𝕜 (StrongDual 𝕜 X))
    (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))

Tactic:
exact WeakDual.isCompact_of_bounded_of_closed
    (WeakDual.isBounded_closure ((inclusionInDoubleDual 𝕜 X).lipschitz.isBounded_image hb))
    isClosed_closure

Premises used: WeakDual.isBounded_closure, WeakDual.isCompact_of_bounded_of_closed, isClosed_closure
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
simp :
  IsClosed[ContinuousLinearMap.topologicalSpace]
    (⋂ x ∈ s,
      {y : E →L[𝕜] 𝕜 |
        norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ≤
          1})
⊢ IsClosed[ContinuousLinearMap.topologicalSpace] (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) s)

Tactic:
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]

Premises used: LinearMap.polar_eq_iInter, LinearMap.flip_apply
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    (⋂ x ∈ s,
      {y : E →L[𝕜] 𝕜 |
        norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ≤
          1})

Tactic:
isClosed_biInter fun z _ => ?_

Premises used: isClosed_biInter
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
refine :
  ∀ z ∈ s,
    IsClosed[ContinuousLinearMap.topologicalSpace]
      {y : E →L[𝕜] 𝕜 |
        norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤
          1}
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    (⋂ x ∈ s,
      {y : E →L[𝕜] 𝕜 |
        norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ≤
          1})

Tactic:
refine isClosed_biInter fun z _ => ?_

Premises used: isClosed_biInter
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
z : E
h : z ∈ s
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    {y : E →L[𝕜] 𝕜 |
      norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤
        1}

Tactic:
isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm

Premises used: Set.Mem, setOf, Continuous.norm, isClosed_Iic, ContinuousLinearMap.continuous, Set.preimage, ContinuousLinearMap.apply, IsClosed.preimage, Set.Iic, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
z : E
h : z ∈ s
⊢ IsClosed[ContinuousLinearMap.topologicalSpace]
    {y : E →L[𝕜] 𝕜 |
      norm.{u_1} (E := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤
        1}

Tactic:
exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm

Premises used: Continuous.norm, isClosed_Iic, ContinuousLinearMap.continuous, ContinuousLinearMap.apply, IsClosed.preimage, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (Function.comp (α := (Set (E →L[𝕜] 𝕜))ᵒᵈ) (β := Set (E →L[𝕜] 𝕜))
      (LinearMap.polar (𝕜 := 𝕜) (LinearMap.flip (LinearMap.flip (topDualPairing 𝕜 E))) : (s : Set (E →L[𝕜] 𝕜)) → Set E)
      ((⇑OrderDual.ofDual : (a : (Set (E →L[𝕜] 𝕜))ᵒᵈ) → Set (E →L[𝕜] 𝕜)) : (a : (Set (E →L[𝕜] 𝕜))ᵒᵈ) → Set (E →L[𝕜] 𝕜))
      (LinearMap.polar (𝕜 := 𝕜) (LinearMap.flip (topDualPairing 𝕜 E)) s : Set (E →L[𝕜] 𝕜)))

Tactic:
simpa [LinearMap.flip_flip] using
          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E := E)).continuous

Premises used: NormedSpace.isClosed_polar, ContinuousLinearMap.continuous, ContinuousLinearMap.apply, IsClosed.preimage, LinearMap.flip_flip
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
pos : ∀ (c_zero : c = 0), Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
neg : ∀ (c_zero : ¬c = 0), Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')

Tactic:
by_cases c_zero : c = 0
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : c = 0
pos : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (HSMul.hSMul (α := 𝕜) 0 x')
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')

Tactic:
simp only [c_zero, inv_zero, zero_smul]

Premises used: inv_zero, zero_smul
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : c = 0
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (HSMul.hSMul (α := 𝕜) 0 x')

Tactic:
(topDualPairing 𝕜 E).flip.zero_mem_polar _

Premises used: LinearMap.zero_mem_polar, topDualPairing, LinearMap.flip
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
⊢ ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)

Tactic:
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
z : E
hzs : z ∈ s
rw : ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖

Tactic:
rw [eq z]
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c⁻¹‖ * ‖c‖

Tactic:
apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)

Premises used: mul_le_mul, le_of_eq, norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
⊢ ∀ z ∈ s, ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖

Tactic:
have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
    intro z hzs
    rw [eq z]
    apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
le : ∀ z ∈ s, ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖c⁻¹‖ * ‖c‖ = 1

Tactic:
simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]

Premises used: norm_eq_zero, Ne, norm_inv, not_false_iff, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
le : ∀ z ∈ s, ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖c⁻¹‖ * ‖c‖ = 1

Tactic:
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by
    simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c‖
c_zero : ¬c = 0
eq :
  ∀ (z : E),
    ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ = ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜)
le : ∀ z ∈ s, ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
neg neg₁ neg₂ neg₃ :
  ∀ (le : ∀ z ∈ s, ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ 1) (cancel : ‖c⁻¹‖ * ‖c‖ = 1),
    Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')

Tactic:
rwa [cancel] at le
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) x'
⊢ ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1

Tactic:
rw [StrongDual.mem_polar_iff] at hx'

Premises used: StrongDual.mem_polar_iff
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
simp : ∀ (hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1), ‖x'‖ ≤ ‖c‖ / r
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (closedBall 0 (‖c‖ / r)) x'

Tactic:
simp only [mem_closedBall_zero_iff, mem_ball_zero_iff] at *

Premises used: mem_closedBall_zero_iff, mem_ball_zero_iff