𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
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
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : ¬x ∈ a • s
⊢ a ≤ gauge s x
rw [starConvex_zero_iff] at hs₀
case intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hx : ¬x ∈ a • s
r : ℝ
hr : 0 < r
h : ∀ (a : ℝ), r ≤ ‖a‖ → {x} ⊆ a • s
⊢ a ≤ gauge s x
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
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
obtain ⟨r, hr, h⟩ := hs₂
case intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hx : ¬x ∈ a • s
r : ℝ
hr : 0 < r
h : ∀ (a : ℝ), r ≤ ‖a‖ → {x} ⊆ a • s
⊢ ∀ (b : ℝ), b ∈ {r | 0 < r ∧ x ∈ r • s} → a ≤ b
case intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hx : ¬x ∈ a • s
r : ℝ
hr : 0 < r
h : ∀ (a : ℝ), r ≤ ‖a‖ → {x} ⊆ a • s
⊢ a ≤ gauge s x
refine' le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ _
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
⊢ a ≤ b
case intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hx : ¬x ∈ a • s
r : ℝ
hr : 0 < r
h : ∀ (a : ℝ), r ≤ ‖a‖ → {x} ⊆ a • s
⊢ ∀ (b : ℝ), b ∈ {r | 0 < r ∧ x ∈ r • s} → a ≤ b
rintro b ⟨hb, x, hx', rfl⟩
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
⊢ (fun x => b • x) x ∈ a • s
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
⊢ a ≤ b
refine' not_lt.1 fun hba => hx _
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ (fun x => b • x) x ∈ a • s
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
⊢ (fun x => b • x) x ∈ a • s
have ha := hb.trans hba
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ a⁻¹ * b ≤ 1

case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ (fun x => a • x) ((a⁻¹ * b) • x) = (fun x => b • x) x
case intro.intro.intro.intro.intro
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ (fun x => b • x) x ∈ a • s
refine' ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) _, _⟩
no goals
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ 0 ≤ a⁻¹ * b
positivity
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ a⁻¹ * b ≤ 1
rw [← div_eq_inv_mul]
no goals
case intro.intro.intro.intro.intro.refine'_1
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1
exact div_le_one_of_le hba.le ha.le
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ a • (a⁻¹ * b) • x = b • x
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ (fun x => a • x) ((a⁻¹ * b) • x) = (fun x => b • x) x
dsimp only
no goals
case intro.intro.intro.intro.intro.refine'_2
𝕜 : Type ?u.88359
E : Type u_1
F : Type ?u.88365
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : 0 < r
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hx : ¬(fun x => b • x) x ∈ a • s
h : ∀ (a : ℝ), r ≤ ‖a‖ → {(fun x => b • x) x} ⊆ a • s
hba : b < a
ha : 0 < a
⊢ a • (a⁻¹ * b) • x = b • x
rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']