awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
have h : ∀ (χ : α) (hp : p χ) (hy : dist (y χ) x < δ) (hz : dist (z χ) x < δ), ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Tactic: filter_upwards [hp, hy δ hδ, hz δ hδ] with χ hp hy hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
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
have refine : ∀ᶠ (x : α) in f, ∀ (a : E) (b : a ∈ [y x -[ℝ] z x]), a ∈ s → r x a
Tactic: refine seg.mp <| .mono ?_ (fun _ => forall₂_imp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
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
⊢ ∀ᶠ (x : α) in f, ∀ (a : E) (b : a ∈ [y x -[ℝ] z x]), a ∈ s → r x a
have apply : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, p.2 ∈ s → r p.1 p.2
Tactic: apply Eventually.segment_of_prod_nhds hy hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 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‖
have apply : ‖x‖ ≤
  norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
    ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))
Tactic: apply le_antisymm (double_dual_bound 𝕜 E x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ ≤
    norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))
have 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))
Tactic: obtain ⟨g, hg⟩ := exists_dual_vector'' 𝕜 x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
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 (E := StrongDual 𝕜 (StrongDual 𝕜 E))
      ((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E))
have grw : ‖x‖ ≤
  norm.{v} (E := 𝕜)
    ((((inclusionInDoubleDual 𝕜 E : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) :
          (a : StrongDual 𝕜 E) → 𝕜)
        g :
      𝕜)
Tactic: grw [← (inclusionInDoubleDual 𝕜 E x).unit_le_opNorm g hg.left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
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‖
⊢ ‖x‖ ≤ M
have rw : norm (E := StrongDual 𝕜 (StrongDual 𝕜 E))
    ((inclusionInDoubleDualLi 𝕜 : (a : E) → StrongDual 𝕜 (StrongDual 𝕜 E)) x : StrongDual 𝕜 (StrongDual 𝕜 E)) ≤
  M
Tactic: rw [← (inclusionInDoubleDualLi (E := E) 𝕜).norm_map x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
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 (closure S)
have 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)))
Tactic: rw [(isEmbedding_inclusionInDoubleDualWeak 𝕜 X).closure_eq_preimage_closure_image]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.DoubleDual (goal)
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.{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)))
have apply : IsCompact (X := WeakDual 𝕜 (StrongDual 𝕜 X))
  (closure ((⇑(inclusionInDoubleDualWeak 𝕜 X) : (a : WeakSpace 𝕜 X) → WeakDual 𝕜 (StrongDual 𝕜 X)) '' S))
Tactic: apply (isEmbedding_inclusionInDoubleDualWeak 𝕜 X).isCompact_preimage' _ hrange
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[ContinuousLinearMap.topologicalSpace] (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) s)
have 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})
Tactic: simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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})
have 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}
Tactic: refine isClosed_biInter fun z _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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‖
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
have pos : ∀ (c_zero : c = 0), Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
Tactic: by_cases c_zero : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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')
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
have neg : ∀ (c_zero : ¬c = 0), Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
Tactic: by_cases c_zero : c = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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) (c⁻¹ • x')
have pos : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (HSMul.hSMul (α := 𝕜) 0 x')
Tactic: simp only [c_zero, inv_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (hypothesis)
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) (c⁻¹ • x')
have eq : ∀ (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⁻¹ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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
⊢ ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((x' : (a : E) → 𝕜) z : 𝕜)‖ ≤ ‖c⁻¹‖ * ‖c‖
have rw : ‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ ‖c⁻¹‖ * ‖c‖
Tactic: rw [eq z]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (hypothesis)
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 : 𝕜)
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
have le : ∀ 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 _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (hypothesis)
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‖
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
have cancel : ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) (c⁻¹ • x')
have 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')
Tactic: rwa [cancel] at le
Cleared hypotheses: le, cancel
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (hypothesis)
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'
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (closedBall 0 (‖c‖ / r)) x'
have hx'₁ : ∀ (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'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (closedBall 0 (‖c‖ / r)) x'
have simp : ∀ (hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1), ‖x'‖ ≤ ‖c‖ / r
Tactic: simp only [mem_closedBall_zero_iff, mem_ball_zero_iff] at *
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (hypothesis)
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), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
⊢ ‖x'‖ ≤ ‖c‖ / r
have hcr : 0 < ‖c‖ / r
Tactic: have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
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), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r
have refine : ∀ (x : E) (h₁ : r / ‖c‖ ≤ ‖x‖) (h₂ : ‖x‖ < r), norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ / r * ‖x‖
Tactic: refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) (closedBall 0 r⁻¹)
have refine : Subset (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) (closedBall 0 r⁻¹)
Tactic: refine Subset.antisymm ?_ (closedBall_inv_subset_polar_closedBall 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (closedBall 0 r⁻¹) x'
have simp : ‖x'‖ ≤ r⁻¹
Tactic: simp only [mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
⊢ ‖x'‖ ≤ r⁻¹
have refine : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_3} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ r⁻¹ * ‖z‖
Tactic: refine ContinuousLinearMap.opNorm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (closedBall 0 r⁻¹)
have rw : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (closedBall 0 r))
Tactic: rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
rw : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (closedBall 0 r))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (closedBall 0 r⁻¹)
have rw₁ : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r))
  (polar 𝕜 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 r)))
Tactic: rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
rw : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (closedBall 0 r))
rw₁ :
  Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r))
    (polar 𝕜 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 r)))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (closedBall 0 r⁻¹)
have rw₂ : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (ball 0 r))
Tactic: rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
have obtain : ∀ (a : 𝕜) (ha : 1 < ‖a‖), IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
Tactic: obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
a : 𝕜
ha : 1 < ‖a‖
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
have obtain : ∀ (r : ℝ) (r_pos : 0 < r) (r_ball : ball 0 r ⊆ s), IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
Tactic: obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhds
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
| closedBall 0 r
have rw : closedBall 0 r⁻¹⁻¹
Tactic: rw [← inv_inv r]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r)
have conv_rhs : Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)
Tactic: conv_rhs => rw [← inv_inv r]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)
have rw : Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
  (polar 𝕜 (closedBall 0 r⁻¹))
Tactic: rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
rw :
  Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
    (polar 𝕜 (closedBall 0 r⁻¹))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)
have rw₁ : Eq (α := Set (StrongDual 𝕜 E))
  (⋂₀ (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
  (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
Tactic: rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
rw :
  Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
    (polar 𝕜 (closedBall 0 r⁻¹))
rw₁ :
  Eq (α := Set (StrongDual 𝕜 E))
    (⋂₀ (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
    (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)
have rw₂ : Eq (α := Set (StrongDual 𝕜 E))
  (LinearMap.polar (𝕜 := 𝕜) (E := E) (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
  (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
Tactic: rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Dual (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ AbsConvex.{u_1, u_3} 𝕜 (E := F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B s)
have rw : AbsConvex.{u_1, u_3} 𝕜 (E := F)
  (⋂ x ∈ s,
    Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) (Metric.closedBall 0 1))
Tactic: rw [polar_eq_biInter_preimage]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Extr (goal)
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖
have grw : ‖f x + y‖ ≤ ‖f c‖ + ‖y‖
Tactic: grw [hy.norm_add, norm_add_le, hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Extr (goal)
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
grw : ‖f x + y‖ ≤ ‖f c‖ + ‖y‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖
have grw₁ : ‖f x‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
Tactic: grw [hy.norm_add, norm_add_le, hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Extr (goal)
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
grw : ‖f x + y‖ ≤ ‖f c‖ + ‖y‖
grw₁ : ‖f x‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖
have grw₂ : ‖f c‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
Tactic: grw [hy.norm_add, norm_add_le, hx]