-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_add_le (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (x y : E) :
    gauge s (x + y) ≤ gauge s x + gauge s y

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ 0 ≤ a + b

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => 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)

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 + ε

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ε))

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
⊢ gauge s ((fun x => a • x) x + y) < gauge s ((fun x => a • x) x) + gauge s y + ε

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ gauge s ((fun x => a • x) x + (fun x => b • x) y) < gauge s ((fun x => a • x) x) + gauge s ((fun x => 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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
⊢ gauge s ((fun x => a • x) x + y) < gauge s ((fun x => 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ε))

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ gauge s ((fun x => a • x) x + (fun x => b • x) y) < gauge s ((fun x => a • x) x) + gauge s ((fun x => b • x) y) + ε

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ a • x + b • y ∈ (a + b) • s

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

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ a • x + b • y ∈ a • s + b • s

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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:
refine le_of_forall_pos_lt_add fun ε hε => ?_

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 + ε

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x => b • x) y) + ε / 2
⊢ a + b < gauge s (a • x) + gauge s (b • y) + ε

Tactic:
linarith

Result:
no goals