awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • x ∈ s
have h₁ : Membership.mem (γ := Set E) {x : E | gauge s x < 1} (r • x)
Tactic: apply gauge_lt_one_subset_self hc hs₀ ha
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} (r • x)
have h₁ : r • gauge s x < 1
Tactic: rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ x ∈ closure[inst_2] s
have this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
Tactic: have : ∀ᶠ r : ℝ in 𝓝[<] 1, r • x ∈ s := by
    filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩
    apply gauge_lt_one_subset_self hc hs₀ ha
    rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]
    exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ x ∈ closure[inst_2] s
have refine : Tendsto (fun (x_1 : ℝ) ↦ x_1 • x) (𝓝[<] 1) (𝓝 x)
Tactic: refine mem_closure_of_tendsto ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)
have refine : ∀ (ε : ℝ) (hε : 0 < ε), ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
Tactic: refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
have hs₁ : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
Tactic: rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs
Cleared hypotheses: hs, hε
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
ε : ℝ
hs : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
have h : ∀ (x : E) (hx : x ∈ ε • s), gauge s x ∈ Icc 0 ε
Tactic: filter_upwards [hs] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ ContinuousAt (gauge s) 0
have rw : Tendsto (gauge s) (𝓝 0) (𝓝 0)
Tactic: rw [ContinuousAt, gauge_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ ContinuousAt (gauge s) x
have ha : Absorbent ℝ s
Tactic: have ha : Absorbent ℝ s := absorbent_nhds_zero hs₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
⊢ ContinuousAt (gauge s) x
have refine : ∀ (ε : ℝ) (hε₀ : 0 < ε), ∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)
Tactic: refine (nhds_basis_Icc_pos _).tendsto_right_iff.2 fun ε hε₀ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)
have rw : ∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
Tactic: rw [← map_add_left_nhds_zero, eventually_map]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
⊢ ∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
have this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
Tactic: have : ε • s ∩ -(ε • s) ∈ 𝓝 0 :=
    inter_mem ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀)
      (neg_mem_nhds_zero _ ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
⊢ ∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
have h : ∀ (y : E) (hy : y ∈ ε • s ∩ -(ε • s)), gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
Tactic: filter_upwards [this] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
have h : gauge s x - ε ≤ gauge s (x + y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
h : gauge s x - ε ≤ gauge s (x + y)
⊢ gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
have h₁ : gauge s (x + y) ≤ gauge s x + ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x - ε ≤ gauge s (x + y)
have h : gauge s x ≤ gauge s (x + y) + ε
Tactic: rw [sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s (x + y) + gauge s (-y) ≤ gauge s (x + y) + ε
have grw : gauge s (x + y) + ε ≤ gauge s (x + y) + ε
Tactic: grw [gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x ≤ gauge s (x + y) + ε
have gauge : gauge s x = gauge s (x + y + -y)
Tactic: calc
      gauge s x = gauge s (x + y + (-y)) := by simp
      _ ≤ gauge s (x + y) + gauge s (-y) := gauge_add_le hc ha _ _
      _ ≤ gauge s (x + y) + ε := by grw [gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
gauge : _root_.gauge s x = _root_.gauge s (x + y + -y)
⊢ _root_.gauge s x ≤ _root_.gauge s (x + y) + ε
have gauge₁ : _root_.gauge s (x + y) + _root_.gauge s (-y) ≤ _root_.gauge s (x + y) + ε
Tactic: calc
      gauge s x = gauge s (x + y + (-y)) := by simp
      _ ≤ gauge s (x + y) + gauge s (-y) := gauge_add_le hc ha _ _
      _ ≤ gauge s (x + y) + ε := by grw [gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x + gauge s y ≤ gauge s x + ε
have grw : gauge s x + ε ≤ gauge s x + ε
Tactic: grw [gauge_le_of_mem hε₀.le hy.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s (x + y) ≤ gauge s x + ε
have gauge : gauge s x + gauge s y ≤ gauge s x + ε
Tactic: calc
      gauge s (x + y) ≤ gauge s x + gauge s y := gauge_add_le hc ha _ _
      _ ≤ gauge s x + ε := by grw [gauge_le_of_mem hε₀.le hy.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ {x : E | gauge s x < 1} = interior s
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x), x ∈ interior s
Tactic: refine Subset.antisymm (fun x hx ↦ ?_) (interior_subset_gauge_lt_one s)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
x : E
hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
⊢ x ∈ interior s
have rcases : ∀ (y : E) (hys : y ∈ s) (hxy : x ∈ openSegment ℝ 0 y), x ∈ interior s
Tactic: rcases mem_openSegment_of_gauge_lt_one (absorbent_nhds_zero hs₀) hx with ⟨y, hys, hxy⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ gauge s x = 1 ↔ x ∈ frontier s
have rw : x ∈ closure[inst_2] s ∧ x ∉ interior s ↔ x ∈ frontier s
Tactic: rw [eq_iff_le_not_lt, gauge_le_one_iff_mem_closure hc hs₀, gauge_lt_one_iff_mem_interior hc hs₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst_5 : TopologicalSpace E
inst_6 : ContinuousSMul ℝ E
hs : IsOpen[inst_5] s
⊢ (gaugeSeminorm (s := s) hs₀ hs₁ hs₂).ball 0 1 = s
have rw : {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := s) hs₀ hs₁ hs₂ : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = s
Tactic: rw [Seminorm.ball_zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
⊢ gauge (p.ball 0 1) = (⇑p : (a : E) → ℝ)
have h : ∀ (x : E), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
have h : ∀ (hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
Tactic: obtain hp | hp := { r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1 }.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
h : ∀ (hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
have h₁ : ∀ (hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
Tactic: obtain hp | hp := { r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1 }.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
have h : Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [gauge, hp, Real.sInf_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
⊢ Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
have h : ∀ (h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ False
have hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: have hpx : 0 < p x := (apply_nonneg _ _).lt_of_ne h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ False
have hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ False
have h₁ : (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ))⁻¹ • x ∈ p.ball 0 1
Tactic: refine hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ))⁻¹ • x ∈ p.ball 0 1
have h₁ : (p : (a : E) → ℝ) x < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpx₂),
      inv_mul_lt_iff₀ hpx₂, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
have h : ∀ (r : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} r → (p : (a : E) → ℝ) x ≤ r
Tactic: refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
h : ∀ (r : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} r → (p : (a : E) → ℝ) x ≤ r
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
have h₁ : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r) (ε : ℝ) (hε : 0 < ε),
  r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
Tactic: refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ p.ball 0 1
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
⊢ (p : (a : E) → ℝ) ((fun (x : E) ↦ r • x) y) ≤ r
have hy₁ : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
Tactic: rw [p.mem_ball_zero] at hy
Cleared hypotheses: hy, hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
⊢ (p : (a : E) → ℝ) ((fun (x : E) ↦ r • x) y) ≤ r
have h : HMul.hMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ) ≤ r
Tactic: rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
⊢ r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
have hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
Tactic: have hpε : 0 < p x + ε := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
have h : (HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε)⁻¹ • x ∈ p.ball 0 1
Tactic: refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ (HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε)⁻¹ • x ∈ p.ball 0 1
have h : (p : (a : E) → ℝ) x < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
Tactic: rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε),
      inv_mul_lt_iff₀ hpε, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ gauge (ball 0 1) x = ‖x‖
have rw : gauge (Seminorm.ball (normSeminorm ℝ E) 0 1) x = ‖x‖
Tactic: rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
rw : gauge (Seminorm.ball (normSeminorm ℝ E) 0 1) x = ‖x‖
⊢ gauge (ball 0 1) x = ‖x‖
have rw₁ : (normSeminorm ℝ E : (a : E) → ℝ) x = ‖x‖
Tactic: rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
rw : gauge (Seminorm.ball (normSeminorm ℝ E) 0 1) x = ‖x‖
rw₁ : (normSeminorm ℝ E : (a : E) → ℝ) x = ‖x‖
⊢ gauge (ball 0 1) x = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ gauge (ball 0 r) x = ‖x‖ / r
have inl : ∀ (hr : LE.le (α := ℝ) 0 0), gauge (ball 0 0) x = ‖x‖ / 0
Tactic: rcases hr.eq_or_lt with rfl | hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
inl : ∀ (hr : LE.le (α := ℝ) 0 0), gauge (ball 0 0) x = ‖x‖ / 0
⊢ gauge (ball 0 r) x = ‖x‖ / r
have inr : ∀ (hr : 0 < r), gauge (ball 0 r) x = ‖x‖ / r
Tactic: rcases hr.eq_or_lt with rfl | hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r
have inr : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 1) x → Membership.mem (γ := Set E) (ball 0 1) (-x)
Tactic: rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
    abs_of_nonneg hr.le, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), Membership.mem (γ := Set E) (ball 0 1) x → Membership.mem (γ := Set E) (ball 0 1) (-x)
have inr : ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1
Tactic: simp_rw [mem_ball_zero_iff, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ gauge (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 0) x = 0 x
have simp : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
Tactic: simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero,
    norm_eq_zero, inv_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
have inl : ∀ (hx : ‖x‖ = 0), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
Tactic: rcases (norm_nonneg x).eq_or_lt' with hx | hx