-- Mathlib/Analysis/Convex/Gauge.lean
theorem le_gauge_of_not_mem (hs₀ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s {x}) (hx : x ∉ a • s) :
    a ≤ gauge s x

Proof state:
case intro.intro.intro.intro.intro.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a • (a⁻¹ * b) • x = b • x

Tactic:
rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']

Result:
no goals

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

Tactic:
obtain ⟨r, hr, h⟩ := hs₂.exists_pos

Result:
case intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
⊢ a ≤ b

Tactic:
refine not_lt.1 fun hba => hx ?_

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
⊢ (fun x => b • x) x ∈ a • s

Proof state:
case intro.intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a⁻¹ * b ≤ 1

Tactic:
rw [← div_eq_inv_mul]

Result:
case intro.intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ (fun x => b • x) x ∈ a • s

Tactic:
refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a⁻¹ * b ≤ 1

case intro.intro.intro.intro.intro.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ (fun x => a • x) ((a⁻¹ * b) • x) = (fun x => b • x) x

Proof state:
case intro.intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1

Tactic:
exact div_le_one_of_le₀ hba.le ha.le

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x

Tactic:
rw [starConvex_zero_iff] at hs₀

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

Proof state:
case intro.intro.intro.intro.intro.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ (fun x => a • x) ((a⁻¹ * b) • x) = (fun x => b • x) x

Tactic:
dsimp only

Result:
case intro.intro.intro.intro.intro.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ a • (a⁻¹ * b) • x = b • x

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
⊢ (fun x => b • x) x ∈ a • s

Tactic:
have ha := hb.trans hba

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ (fun x => b • x) x ∈ a • s

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ 0 ≤ a⁻¹ * b

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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
⊢ ∀ b ∈ {r | 0 < r ∧ x ∈ r • s}, a ≤ b

Tactic:
rintro b ⟨hb, x, hx', rfl⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : 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 => b • x) x}
hx : (fun x => b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s
⊢ a ≤ b