awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
rw : gauge (- -s) (-x) = gauge s (-x)
rw₁ rw₂ : gauge s (-x) = gauge s (-x)
⊢ gauge (-s) x = gauge s (-x)

Tactic:
rw [← gauge_neg_set_neg, neg_neg]

Premises used: neg_neg, gauge_neg_set_neg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
inl : ∀ (ha : LE.le (α := ℝ) 0 0) (hx : x ∈ HSMul.hSMul (α := ℝ) 0 s), gauge s x ≤ 0
inr : ∀ (ha' : 0 < a), gauge s x ≤ a
⊢ gauge s x ≤ a

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
ha : LE.le (α := ℝ) 0 0
hx : x ∈ HSMul.hSMul (α := ℝ) 0 s
inl : gauge s 0 ≤ 0
inl₁ inl₂ : LE.le (α := ℝ) 0 0
⊢ gauge s x ≤ 0

Tactic:
rw [mem_singleton_iff.1 (zero_smul_set_subset _ hx), gauge_zero]

Premises used: Set.mem_singleton_iff, Iff.mp, gauge_zero, Set.zero_smul_set_subset
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a

Tactic:
csInf_le gauge_set_bddBelow ⟨ha', hx⟩

Premises used: gauge, _private.0.gauge_set_bddBelow, And.intro, csInf_le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a

Tactic:
exact csInf_le gauge_set_bddBelow ⟨ha', hx⟩

Premises used: _private.0.gauge_set_bddBelow, And.intro, csInf_le
-- Module: Mathlib.Analysis.Convex.Gauge
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
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) {x : E | gauge s x ≤ a} x ↔
      Membership.mem (γ := Set E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s) x
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Gauge
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 ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
⊢ Membership.mem (γ := Set E) {x : E | gauge s x ≤ a} x ↔
    Membership.mem (γ := Set E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s) x

Tactic:
simp_rw [Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s

Tactic:
⟨fun h r hr => ?_, fun h => le_of_forall_pos_lt_add fun ε hε => ?_⟩

Premises used: le_of_forall_pos_lt_add, Iff.intro
-- Module: Mathlib.Analysis.Convex.Gauge
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 : ∀ (h : gauge s x ≤ a) (r : ℝ) (hr : a < r), x ∈ r • s
h₁ : ∀ (h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s) (ε : ℝ) (hε : 0 < ε), gauge s x < a + ε
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s

Tactic:
refine ⟨fun h r hr => ?_, fun h => le_of_forall_pos_lt_add fun ε hε => ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ 0 < r

Tactic:
have hr' := ha.trans_lt hr
-- Module: Mathlib.Analysis.Convex.Gauge
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
h₁ : r⁻¹ • x ∈ s
⊢ x ∈ r • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hr'.ne']

Premises used: LT.lt.ne', Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
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
h₁ : ∀ (δ : ℝ) (δ_pos : 0 < δ) (hδr : δ < r) (hδ : x ∈ δ • s), r⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s

Tactic:
obtain ⟨δ, δ_pos, hδr, hδ⟩ := exists_lt_of_gauge_lt hs₂ (h.trans_lt hr)

Premises used: exists_lt_of_gauge_lt, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Gauge
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : r⁻¹ • x ∈ s), r⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s

Tactic:
rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this

Premises used: smul_smul, mul_inv_cancel_right₀, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
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
h₁ : (r⁻¹ * δ) • δ⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s

Tactic:
suffices (r⁻¹ * δ) • δ⁻¹ • x ∈ s by rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ δ⁻¹ • x ∈ s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ

Premises used: LT.lt.ne', Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ 0 ≤ r⁻¹ * δ

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Gauge
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
h₁ : r⁻¹ * δ ≤ 1
⊢ (r⁻¹ * δ) • δ⁻¹ • x ∈ s

Tactic:
refine hs₁.smul_mem_of_zero_mem hs₀ hδ ⟨by positivity, ?_⟩

Premises used: And.intro, Convex.smul_mem_of_zero_mem
-- Module: Mathlib.Analysis.Convex.Gauge
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
h₁ : δ ≤ r
⊢ r⁻¹ * δ ≤ 1

Tactic:
rw [inv_mul_le_iff₀ hr', mul_one]

Premises used: inv_mul_le_iff₀, mul_one
-- Module: Mathlib.Analysis.Convex.Gauge
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

Tactic:
hδr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
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

Tactic:
exact hδr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
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
linarith₃ : a + ε / 2 < 0 → 2 * (0 - a) + (0 - ε) + (2 * a + 1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : a + ε / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ a + ε / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Gauge
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
linarith₃ : a + ε / 2 ≤ a → 0 - ε + (2 * a + 1 * ε - 2 * a) = 0
⊢ a < a + ε / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Gauge
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
linarith₃ : a + ε ≤ gauge s x → 0 - ε + 2 * (a + ε - gauge s x) + (2 * gauge s x - (2 * a + 1 * ε)) = 0
linarith₄ : a + ε ≤ gauge s x → GT.gt (α := ℝ) 2 0
⊢ gauge s x < a + ε

Tactic:
linarith [gauge_le_of_mem (by linarith) <| h (a + ε / 2) (by linarith)]

Premises used: gauge_le_of_mem, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
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
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x < a} (⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x : E
h : gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔
    Membership.mem (γ := Set E) (⋃ (r : ℝ), ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s) x

Tactic:
simp_rw [mem_setOf, mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_setOf
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x : E
⊢ gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s

Tactic:
⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
      (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩

Premises used: gauge, gauge_le_of_mem, LT.lt.le, _private.0.gauge_lt_eq'.match_3, exists_lt_of_gauge_lt, LT.lt, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x : E
⊢ gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s

Tactic:
exact
    ⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
      (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
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
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x < a} (⋃ r ∈ Ioo 0 a, r • s)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x : E
h : gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < a} x ↔ Membership.mem (γ := Set E) (⋃ r ∈ Ioo 0 a, r • s) x

Tactic:
simp_rw [mem_setOf, mem_iUnion, exists_prop, mem_Ioo, and_assoc]

Premises used: Set.mem_Ioo, Set.mem_iUnion, exists_prop, Set.mem_setOf, and_assoc
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x : E
⊢ gauge s x < a ↔ ∃ (i : ℝ), 0 < i ∧ i < a ∧ x ∈ i • s

Tactic:
⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
      (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩

Premises used: gauge, gauge_le_of_mem, LT.lt.le, _private.0.gauge_lt_eq.match_2, exists_lt_of_gauge_lt, LT.lt, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Gauge
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
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
⊢ ∃ y ∈ s, x ∈ openSegment ℝ 0 y

Tactic:
rcases exists_lt_of_gauge_lt absorbs hgauge with ⟨r, hr₀, hr₁, y, hy, rfl⟩

Premises used: exists_lt_of_gauge_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
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

Tactic:
⟨y, hy, 1 - r, r, ?_⟩

Premises used: HSub.hSub, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
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
refine : 0 < 1 - r ∧ 0 < r ∧ 1 - r + r = 1 ∧ HSMul.hSMul (β := E) (1 - r) 0 + r • y = (fun (x : E) ↦ r • x) y
⊢ ∃ y_1 ∈ s, (fun (x : E) ↦ r • x) y ∈ openSegment ℝ 0 y_1

Tactic:
refine ⟨y, hy, 1 - r, r, ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ 0 < 1 - r ∧ 0 < r ∧ 1 - r + r = 1 ∧ HSMul.hSMul (β := E) (1 - r) 0 + r • y = (fun (x : E) ↦ r • x) y

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
⊢ {x : E | gauge s x < 1} ⊆ s

Tactic:
fun _x hx ↦
  let ⟨_y, hys, hx⟩ := mem_openSegment_of_gauge_lt_one absorbs hx
  hs.openSegment_subset h₀ hys hx

Premises used: _private.0.gauge_lt_one_subset_self.match_1, Membership.mem, Convex.openSegment_subset, Set.Subset, mem_openSegment_of_gauge_lt_one
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ x ∈ HSMul.hSMul (α := ℝ) 1 s

Tactic:
rwa [one_smul]

Premises used: one_smul
-- Module: Mathlib.Analysis.Convex.Gauge
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

Tactic:
le_of_forall_pos_lt_add fun ε hε => ?_

Premises used: le_of_forall_pos_lt_add
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
absorbs : Absorbent ℝ s
x y : E
refine : ∀ (ε : ℝ) (hε : 0 < ε), gauge s (x + y) < gauge s x + gauge s y + ε
⊢ gauge s (x + y) ≤ gauge s x + gauge s y

Tactic:
refine le_of_forall_pos_lt_add fun ε hε => ?_

Premises used: le_of_forall_pos_lt_add
-- Module: Mathlib.Analysis.Convex.Gauge
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 < ε
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 + ε
⊢ gauge s (x + y) < gauge s 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ε))

Premises used: lt_add_of_pos_right, gauge, half_pos, exists_lt_of_gauge_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
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
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) + ε
⊢ gauge s ((fun (x : E) ↦ a • x) x + y) < gauge s ((fun (x : E) ↦ a • x) x) + gauge s 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ε))

Premises used: lt_add_of_pos_right, gauge, half_pos, exists_lt_of_gauge_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ 0 ≤ a + b

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Gauge
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
rw : a • x + b • y ∈ a • s + b • s
⊢ a • x + b • y ∈ (a + b) • s

Tactic:
rw [hs.add_smul ha.le hb.le]

Premises used: LT.lt.le, Convex.add_smul
-- Module: Mathlib.Analysis.Convex.Gauge
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 • s + b • s

Tactic:
add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)

Premises used: Set.add_mem_add, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.Gauge
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 • s + b • s

Tactic:
exact add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)

Premises used: Set.add_mem_add, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.Gauge
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
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
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) + ε

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.Gauge
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 < _root_.gauge s ((fun (x : E) ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < _root_.gauge s ((fun (x : E) ↦ b • x) y) + ε / 2
gauge : a + b < _root_.gauge s (a • x) + _root_.gauge s (b • y) + ε
⊢ _root_.gauge s (HAdd.hAdd (α := E) ((fun (x : E) ↦ a • x) x) ((fun (x : E) ↦ b • x) y)) <
    _root_.gauge s ((fun (x : E) ↦ a • x) x) + _root_.gauge s ((fun (x : E) ↦ b • x) 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

Premises used: gauge, gauge_le_of_mem, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
ι : Type u_3
hs : Convex ℝ s
absorbs : Absorbent ℝ s
t : Finset ι
f : ι → E
⊢ gauge s (∑ i ∈ t, f i) ≤ ∑ i ∈ t, gauge s (f i)

Tactic:
Finset.le_sum_of_subadditive _ gauge_zero.le (gauge_add_le hs absorbs) _ _

Premises used: Finset.le_sum_of_subadditive, gauge_add_le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ s ⊆ {x : E | gauge s x ≤ 1}

Tactic:
fun _ => gauge_le_one_of_mem

Premises used: gauge_le_one_of_mem, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Analysis.Convex.Gauge
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}
neg : ∀ (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}

Tactic:
by_cases ha : 0 ≤ a
-- Module: Mathlib.Analysis.Convex.Gauge
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
pos : Convex.{0, u_2} ℝ (E := E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}

Tactic:
rw [gauge_le_eq hs h₀ absorbs ha]

Premises used: gauge_le_eq
-- Module: Mathlib.Analysis.Convex.Gauge
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) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)

Tactic:
convex_iInter fun i => convex_iInter fun _ => hs.smul _

Premises used: Convex.smul, convex_iInter
-- Module: Mathlib.Analysis.Convex.Gauge
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) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)

Tactic:
exact convex_iInter fun i => convex_iInter fun _ => hs.smul _

Premises used: Convex.smul, convex_iInter
-- Module: Mathlib.Analysis.Convex.Gauge
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) ∅

Tactic:
convex_empty (𝕜 := ℝ)

Premises used: convex_empty
-- Module: Mathlib.Analysis.Convex.Gauge
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
h : Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} ∅
⊢ Convex.{0, u_2} ℝ (E := E) {x : E | gauge s x ≤ a}

Tactic:
convert! convex_empty (𝕜 := ℝ)

Premises used: convex_empty
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun x hx => ha <| (gauge_nonneg _).trans hx

Premises used: Iff.mpr, gauge_nonneg, Set.eq_empty_iff_forall_notMem, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Gauge
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
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} ∅

Tactic:
exact eq_empty_iff_forall_notMem.2 fun x hx => ha <| (gauge_nonneg _).trans hx

Premises used: Iff.mpr, gauge_nonneg, Set.eq_empty_iff_forall_notMem, LE.le.trans