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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
this : (r⁻¹ * δ) • δ⁻¹ • x ∈ s
rwa : ∀ (this : (r⁻¹ * δ * δ⁻¹) • x ∈ s), r⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s
have rwa₁ : ∀ (this : r⁻¹ • x ∈ s), r⁻¹ • x ∈ s
Tactic: rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
Cleared hypotheses: 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
⊢ r⁻¹ • x ∈ s
have h₁ : (r⁻¹ * δ) • δ⁻¹ • x ∈ s
Tactic: suffices (r⁻¹ * δ) • δ⁻¹ • x ∈ s by rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
⊢ (r⁻¹ * δ) • δ⁻¹ • x ∈ s
have hδ₁ : δ⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ
Cleared hypotheses: 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : δ⁻¹ • x ∈ s
⊢ (r⁻¹ * δ) • δ⁻¹ • x ∈ s
have h₁ : r⁻¹ * δ ≤ 1
Tactic: refine hs₁.smul_mem_of_zero_mem hs₀ hδ ⟨by positivity, ?_⟩
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : δ⁻¹ • x ∈ s
⊢ r⁻¹ * δ ≤ 1
have h₁ : δ ≤ r
Tactic: rw [inv_mul_le_iff₀ hr', mul_one]
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ 0 ≤ a + ε / 2
have linarith : a + ε / 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ a + ε / 2
have linarith₁ : a + ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 < 0 → 2 / 2 = 1
linarith₁ : a + ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ a + ε / 2
have linarith₂ : a + ε / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 < 0 → 2 / 2 = 1
linarith₁ : a + ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a + ε / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ a + ε / 2
have linarith₃ : a + ε / 2 < 0 → 2 * (0 - a) + (0 - ε) + (2 * a + 1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ a < a + ε / 2
have linarith : a + ε / 2 ≤ a → 2 / 2 = 1
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 ≤ a → 2 / 2 = 1
⊢ a < a + ε / 2
have linarith₁ : a + ε / 2 ≤ a → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 ≤ a → 2 / 2 = 1
linarith₁ : a + ε / 2 ≤ a → HMul.hMul (α := ℝ) 1 2 = 2
⊢ a < a + ε / 2
have linarith₂ : a + ε / 2 ≤ a → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε / 2 ≤ a → 2 / 2 = 1
linarith₁ : a + ε / 2 ≤ a → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a + ε / 2 ≤ a → GT.gt (α := ℝ) 2 0
⊢ a < a + ε / 2
have linarith₃ : a + ε / 2 ≤ a → 0 - ε + (2 * a + 1 * ε - 2 * a) = 0
Tactic: linarith
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ gauge s x < a + ε
have linarith : a + ε ≤ gauge s x → 2 / 2 = 1
Tactic: linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε ≤ gauge s x → 2 / 2 = 1
⊢ gauge s x < a + ε
have linarith₁ : a + ε ≤ gauge s x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε ≤ gauge s x → 2 / 2 = 1
linarith₁ : a + ε ≤ gauge s x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ gauge s x < a + ε
have linarith₂ : a + ε ≤ gauge s x → GT.gt (α := ℝ) 2 0
Tactic: linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]
-- 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
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
ε : ℝ
hε : 0 < ε
linarith : a + ε ≤ gauge s x → 2 / 2 = 1
linarith₁ : a + ε ≤ gauge s x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a + ε ≤ gauge s x → GT.gt (α := ℝ) 2 0
⊢ gauge s x < a + ε
have linarith₃ : a + ε ≤ gauge s x → 0 - ε + 2 * (a + ε - gauge s x) + (2 * gauge s x - (2 * a + 1 * ε)) = 0
Tactic: linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]
-- 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
absorbs : Absorbent ℝ s
a : ℝ
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x < a} (⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s)
have h : ∀ (x : E),
  Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔
    Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s) x
Tactic: ext
-- 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
absorbs : Absorbent ℝ s
a : ℝ
x : E
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔
    Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s) x
have h : gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s
Tactic: simp_rw [mem_setOf, mem_iUnion, exists_prop]
-- 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
absorbs : Absorbent ℝ s
a : ℝ
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x < a} (⋃ r ∈ Ioo 0 a, r • s)
have h : ∀ (x : E), Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔ Membership.mem (γ := Set E) (⋃ r ∈ Ioo 0 a, r • s) x
Tactic: ext
-- 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
absorbs : Absorbent ℝ s
a : ℝ
x : E
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔ Membership.mem (γ := Set E) (⋃ r ∈ Ioo 0 a, r • s) x
have h : gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s
Tactic: simp_rw [mem_setOf, mem_iUnion, exists_prop, mem_Ioo, and_assoc]
-- 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
absorbs : Absorbent ℝ s
hgauge : gauge s x < 1
⊢ ∃ y ∈ s, x ∈ openSegment ℝ 0 y
have rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr₁ : r < 1) (y : E) (hy : y ∈ s) (hgauge : gauge s ((fun (x : E) ↦ r • x) y) < 1),
  ∃ y_1 ∈ s, (fun (x : E) ↦ r • x) y ∈ openSegment ℝ 0 y_1
Tactic: rcases exists_lt_of_gauge_lt absorbs hgauge with ⟨r, hr₀, hr₁, y, hy, rfl⟩
Cleared hypotheses: x, hgauge
-- 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
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun (x : E) ↦ r • x) y) < 1
⊢ ∃ y_1 ∈ s, (fun (x : E) ↦ r • x) y ∈ openSegment ℝ 0 y_1
have refine : 0 < 1 - r ∧ 0 < r ∧ 1 - r + r = 1 ∧ HSMul.hSMul (β := E) (1 - r) 0 + r • y = (fun (x : E) ↦ r • x) y
Tactic: refine ⟨y, hy, 1 - r, r, ?_⟩
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
x y : E
⊢ gauge s (x + y) ≤ gauge s x + gauge s y
have refine : ∀ (ε : ℝ) (hε : 0 < ε), gauge s (x + y) < gauge s x + gauge s y + ε
Tactic: refine le_of_forall_pos_lt_add 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
x y : E
ε : ℝ
hε : 0 < ε
⊢ gauge s (x + y) < gauge s x + gauge s y + ε
have obtain : ∀ (a : ℝ) (ha : 0 < a) (x : E) (hx : x ∈ s) (ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2),
  gauge s ((fun (x : E) ↦ a • x) x + y) < gauge s ((fun (x : E) ↦ a • x) x) + gauge s y + ε
Tactic: obtain ⟨a, ha, ha', x, hx, rfl⟩ :=
    exists_lt_of_gauge_lt absorbs (lt_add_of_pos_right (gauge s x) (half_pos hε))
Cleared hypotheses: x
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
y : E
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
⊢ gauge s ((fun (x : E) ↦ a • x) x + y) < gauge s ((fun (x : E) ↦ a • x) x) + gauge s y + ε
have obtain : ∀ (b : ℝ) (hb : 0 < b) (y : E) (hy : y ∈ s) (hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2),
  gauge s (HAdd.hAdd (α := E) ((fun (x : E) ↦ a • x) x) ((fun (x : E) ↦ b • x) y)) <
    gauge s ((fun (x : E) ↦ a • x) x) + gauge s ((fun (x : E) ↦ b • x) y) + ε
Tactic: obtain ⟨b, hb, hb', y, hy, rfl⟩ :=
    exists_lt_of_gauge_lt absorbs (lt_add_of_pos_right (gauge s y) (half_pos hε))
Cleared hypotheses: y
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
⊢ a • x + b • y ∈ (a + b) • s
have rw : a • x + b • y ∈ a • s + b • s
Tactic: rw [hs.add_smul ha.le hb.le]
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
⊢ a + b < gauge s (a • x) + gauge s (b • y) + ε
have linarith : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → 2 / 2 = 1
Tactic: linarith
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
linarith : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → 2 / 2 = 1
⊢ a + b < gauge s (a • x) + gauge s (b • y) + ε
have linarith₁ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
linarith : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → 2 / 2 = 1
linarith₁ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → HMul.hMul (α := ℝ) 1 2 = 2
⊢ a + b < gauge s (a • x) + gauge s (b • y) + ε
have linarith₂ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
linarith : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → 2 / 2 = 1
linarith₁ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → GT.gt (α := ℝ) 2 0
linarith₃ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → 2 / 2 = 1
linarith₄ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b → GT.gt (α := ℝ) 2 0
⊢ a + b < gauge s (a • x) + gauge s (b • y) + ε
have linarith₆ : gauge s (a • x) + gauge s (b • y) + ε ≤ a + b →
  2 * a - (2 * gauge s (a • x) + 1 * ε) + (2 * b - (2 * gauge s (b • y) + 1 * ε)) +
      2 * (gauge s (a • x) + gauge s (b • y) + ε - (a + b)) =
    0
Tactic: linarith
-- 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
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
⊢ gauge s (HAdd.hAdd (α := E) ((fun (x : E) ↦ a • x) x) ((fun (x : E) ↦ b • x) y)) <
    gauge s ((fun (x : E) ↦ a • x) x) + gauge s ((fun (x : E) ↦ b • x) y) + ε
have gauge : a + b < gauge s (a • x) + gauge s (b • y) + ε
Tactic: calc
    gauge s (a • x + b • y) ≤ a + b := gauge_le_of_mem (by positivity) <| by
      rw [hs.add_smul ha.le hb.le]
      exact add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
    _ < gauge s (a • x) + gauge s (b • y) + ε := by linarith
-- 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
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
have pos : ∀ (ha : 0 ≤ a), Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
Tactic: by_cases ha : 0 ≤ a
-- 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
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
pos : ∀ (ha : 0 ≤ a), Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
have neg : ∀ (ha : ¬0 ≤ a), Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
Tactic: by_cases ha : 0 ≤ a
-- 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
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
have pos : Convex.{0, u_2} ℝ (E := E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)
Tactic: rw [gauge_le_eq hs h₀ absorbs 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
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}
have h : Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} ∅
Tactic: convert! convex_empty (𝕜 := ℝ)
-- 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
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x
have hs₁ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
Tactic: rw [starConvex_zero_iff] at hs₀
Cleared hypotheses: hs₀, hs₂, 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
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x
have obtain : ∀ (r : ℝ) (hr : r > 0) (h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s), a ≤ gauge s x
Tactic: obtain ⟨r, hr, h⟩ := hs₂.exists_pos
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
r : ℝ
hr : r > 0
h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s
⊢ a ≤ gauge s x
have refine : ∀ (b : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • s} b → a ≤ b
Tactic: refine le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
⊢ a ≤ b
have refine : ∀ (hba : b < a), (fun (x : E) ↦ b • x) x ∈ a • s
Tactic: refine not_lt.1 fun hba => hx ?_
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
⊢ (fun (x : E) ↦ b • x) x ∈ a • s
have ha : 0 < a
Tactic: have ha := hb.trans hba
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ (fun (x : E) ↦ b • x) x ∈ a • s
have refine_1 : a⁻¹ * b ≤ 1
Tactic: refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
refine_1 : a⁻¹ * b ≤ 1
⊢ (fun (x : E) ↦ b • x) x ∈ a • s
have refine_2 : Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ a • x) ((a⁻¹ * b) • x)) ((fun (x : E) ↦ b • x) x)
Tactic: refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a⁻¹ * b ≤ 1
have refine_1 : b / a ≤ 1
Tactic: rw [← div_eq_inv_mul]
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a • (a⁻¹ * b) • x = b • x
have refine_2 : (a * (a⁻¹ * b)) • x = b • x
Tactic: rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']
-- 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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
refine_2 : (a * (a⁻¹ * b)) • x = b • x
⊢ a • (a⁻¹ * b) • x = b • x
have refine_2₁ : b • x = b • x
Tactic: rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
⊢ gauge s (a • x) = a • gauge s x
have inl : ∀ (ha : LE.le.{u_3} (α := α) 0 0),
  gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
inl :
  ∀ (ha : LE.le.{u_3} (α := α) 0 0),
    gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
⊢ gauge s (a • x) = a • gauge s x
have inr : ∀ (ha' : 0 < a), gauge s (a • x) = a • gauge s x
Tactic: obtain rfl | ha' := ha.eq_or_lt