case h
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ x ∈ {x | gauge s x ≤ a} ↔ x ∈ ⋂ (r : ℝ) (_ : a < r), r • s
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
⊢ {x | gauge s x ≤ a} = ⋂ (r : ℝ) (_ : a < r), r • s
ext x
case h
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ), a < i → x ∈ i • s
case h
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ x ∈ {x | gauge s x ≤ a} ↔ x ∈ ⋂ (r : ℝ) (_ : a < r), r • s
simp_rw [Set.mem_iInter, Set.mem_setOf_eq]
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ x ∈ r • s

case h.refine'_2
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ), a < i → x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ gauge s x < a + ε
case h
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ), a < i → x ∈ i • s
refine' ⟨fun h r hr => _, fun h => le_of_forall_pos_lt_add fun ε hε => _⟩
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ x ∈ r • s
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ x ∈ r • s
have hr' := ha.trans_lt hr
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ r⁻¹ • x ∈ s
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ x ∈ r • s
rw [mem_smul_set_iff_inv_smul_mem₀ hr'.ne']
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
case h.refine'_1
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ r⁻¹ • x ∈ s
obtain ⟨δ, δ_pos, hδr, hδ⟩ := exists_lt_of_gauge_lt hs₂ (h.trans_lt hr)
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
suffices (r⁻¹ * δ) • δ⁻¹ • x ∈ s by rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
refine' hs₁.smul_mem_of_zero_mem hs₀ hδ ⟨by positivity, _⟩
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
rw [inv_mul_le_iff hr', mul_one]
no goals
case h.refine'_1.intro.intro.intro
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
exact hδr.le
no goals
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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
⊢ r⁻¹ • x ∈ s
rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
no goals
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : 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⁻¹ * δ
positivity
case h.refine'_2
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ), a < i → x ∈ i • s
ε : ℝ
hε : 0 < ε
hε' : a < a + ε / 2
⊢ gauge s x < a + ε
case h.refine'_2
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ), a < i → x ∈ i • s
ε : ℝ
hε : 0 < ε
⊢ gauge s x < a + ε
have hε' := (lt_add_iff_pos_right a).2 (half_pos hε)
no goals
case h.refine'_2
𝕜 : Type ?u.50346
E : Type u_1
F : Type ?u.50352
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (i : ℝ), a < i → x ∈ i • s
ε : ℝ
hε : 0 < ε
hε' : a < a + ε / 2
⊢ gauge s x < a + ε
exact
  (gauge_le_of_mem (ha.trans hε'.le) <| h _ hε').trans_lt (add_lt_add_left (half_lt_self hε) _)