awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
inr : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 1) x → Membership.mem (γ := Set E) (ball 0 1) (-x)
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
    abs_of_nonneg hr.le, div_eq_inv_mul]

Premises used: LT.lt.le, smul_unitBall_of_pos, gauge_unit_ball, abs_of_nonneg, smul_eq_mul, gauge_smul_left, div_eq_inv_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
inr : ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1
⊢ ∀ (x : E), Membership.mem (γ := Set E) (ball 0 1) x → Membership.mem (γ := Set E) (ball 0 1) (-x)

Tactic:
simp_rw [mem_ball_zero_iff, norm_neg]

Premises used: norm_neg, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1

Tactic:
fun _ => id

Premises used: id
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr_1 : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1

Tactic:
exact fun _ => id

Premises used: id
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
simp : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
⊢ gauge (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 0) x = 0 x

Tactic:
simp only [← singleton_zero, gauge_def', mem_closure_zero_iff_norm, norm_smul, mul_eq_zero,
    norm_eq_zero, inv_eq_zero]

Premises used: norm_eq_zero, inv_eq_zero, gauge_def', norm_smul, mem_closure_zero_iff_norm, mul_eq_zero, Set.singleton_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inl : ∀ (hx : ‖x‖ = 0), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
inr : ∀ (hx : 0 < ‖x‖), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)

Tactic:
rcases (norm_nonneg x).eq_or_lt' with hx | hx

Premises used: LE.le.eq_or_lt', norm_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ Eq (α := ℝ) (sInf (Ioi 0)) 0

Tactic:
csInf_Ioi (a := (0 : ℝ))

Premises used: csInf_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} (Ioi 0)
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)

Tactic:
convert! csInf_Ioi (a := (0 : ℝ))

Premises used: csInf_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} (Ioi 0)

Tactic:
Set.ext fun r ↦ and_iff_left (.inr hx)

Premises used: Set.ext, and_iff_left, Or.inr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} (Ioi 0)

Tactic:
exact Set.ext fun r ↦ and_iff_left (.inr hx)

Premises used: Set.ext, and_iff_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ Eq (α := ℝ) (sInf ∅) 0

Tactic:
Real.sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} ∅
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)

Tactic:
convert! Real.sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} ∅

Tactic:
eq_empty_of_forall_notMem fun r ⟨hr₀, hr⟩ ↦ hx.ne' <| hr.resolve_left hr₀.out.ne'

Premises used: False, Membership.mem.out, Or.resolve_left, _private.0.gauge_closure_zero.match_4, LT.lt.ne', Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} ∅

Tactic:
exact eq_empty_of_forall_notMem fun r ⟨hr₀, hr⟩ ↦ hx.ne' <| hr.resolve_left hr₀.out.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
inl : ∀ (hr : LE.le (α := ℝ) 0 0), gauge (closedBall 0 0) x = ‖x‖ / 0
inr : ∀ (hr' : 0 < r), gauge (closedBall 0 r) x = ‖x‖ / r
⊢ gauge (closedBall 0 r) x = ‖x‖ / r

Tactic:
rcases hr.eq_or_lt with rfl | hr'

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hr : LE.le (α := ℝ) 0 0
inl : Eq (α := ℝ) (0 x) 0
⊢ gauge (closedBall 0 0) x = ‖x‖ / 0

Tactic:
rw [div_zero, closedBall_zero', singleton_zero, gauge_closure_zero]

Premises used: gauge_closure_zero, Metric.closedBall_zero', div_zero, Set.singleton_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hr : LE.le (α := ℝ) 0 0
⊢ Eq (α := ℝ) (0 x) 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
inr : gauge (closedBall 0 r) x ≤ ‖x‖ / r
inr₁ : ‖x‖ / r ≤ gauge (closedBall 0 r) x
⊢ gauge (closedBall 0 r) x = ‖x‖ / r

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
inr : gauge (closedBall 0 r) x ≤ gauge (ball 0 r) x
⊢ gauge (closedBall 0 r) x ≤ ‖x‖ / r

Tactic:
rw [← gauge_ball hr]

Premises used: gauge_ball
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x ≤ gauge (ball 0 r) x

Tactic:
gauge_mono (absorbent_ball_zero hr') ball_subset_closedBall x

Premises used: Metric.ball_subset_closedBall, gauge_mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x ≤ gauge (ball 0 r) x

Tactic:
exact gauge_mono (absorbent_ball_zero hr') ball_subset_closedBall x

Premises used: Metric.ball_subset_closedBall, gauge_mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
this : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x

Tactic:
le_of_tendsto ?_ this

Premises used: le_of_tendsto
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
this : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
refine : Filter.Tendsto (HDiv.hDiv ‖x‖) (𝓝[>] r) (𝓝 (‖x‖ / r))
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x

Tactic:
refine le_of_tendsto ?_ this

Premises used: le_of_tendsto
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
this : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
⊢ Filter.Tendsto (HDiv.hDiv ‖x‖) (𝓝[>] r) (𝓝 (‖x‖ / r))

Tactic:
tendsto_const_nhds.div inf_le_left hr'.ne'

Premises used: tendsto_const_nhds, Filter.Tendsto.div, LT.lt.ne', inf_le_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
this : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
⊢ Filter.Tendsto (HDiv.hDiv ‖x‖) (𝓝[>] r) (𝓝 (‖x‖ / r))

Tactic:
exact tendsto_const_nhds.div inf_le_left hr'.ne'

Premises used: tendsto_const_nhds, Filter.Tendsto.div, LT.lt.ne', inf_le_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
inr : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x

Tactic:
suffices ∀ᶠ R in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x by
        refine le_of_tendsto ?_ this
        exact tendsto_const_nhds.div inf_le_left hr'.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
h : ∀ (R : ℝ) (hR : R ∈ Ioi r), ‖x‖ / R ≤ gauge (closedBall 0 r) x
⊢ ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x

Tactic:
filter_upwards [self_mem_nhdsWithin] with R hR

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
R : ℝ
hR : R ∈ Ioi r
h : gauge (ball 0 R) x ≤ gauge (closedBall 0 r) x
⊢ ‖x‖ / R ≤ gauge (closedBall 0 r) x

Tactic:
rw [← gauge_ball (hr.trans hR.out.le)]

Premises used: Membership.mem.out, gauge_ball, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
R : ℝ
hR : R ∈ Ioi r
⊢ gauge (ball 0 R) x ≤ gauge (closedBall 0 r) x

Tactic:
gauge_mono ?_ (closedBall_subset_ball hR) _

Premises used: Metric.closedBall_subset_ball, gauge_mono
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
R : ℝ
hR : R ∈ Ioi r
h : Absorbent.{0, u_2} ℝ (α := E) (closedBall 0 r)
⊢ gauge (ball 0 R) x ≤ gauge (closedBall 0 r) x

Tactic:
refine gauge_mono ?_ (closedBall_subset_ball hR) _

Premises used: Metric.closedBall_subset_ball, gauge_mono
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
R : ℝ
hR : R ∈ Ioi r
⊢ Absorbent.{0, u_2} ℝ (α := E) (closedBall 0 r)

Tactic:
(absorbent_ball_zero hr').mono ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Absorbent.mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
R : ℝ
hR : R ∈ Ioi r
⊢ Absorbent.{0, u_2} ℝ (α := E) (closedBall 0 r)

Tactic:
exact (absorbent_ball_zero hr').mono ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Absorbent.mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
inl : ∀ (hr : r ≤ 0), r * gauge s x ≤ ‖x‖
inr : ∀ (hr : 0 < r), r * gauge s x ≤ ‖x‖
⊢ r * gauge s x ≤ ‖x‖

Tactic:
obtain hr | hr := le_or_gt r 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

Tactic:
(mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)

Premises used: mul_nonpos_of_nonpos_of_nonneg, gauge_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)

Premises used: mul_nonpos_of_nonpos_of_nonneg, gauge_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
inr : gauge s x ≤ gauge (ball 0 r) x
⊢ r * gauge s x ≤ ‖x‖

Tactic:
rw [mul_comm, ← le_div_iff₀ hr, ← gauge_ball hr.le]

Premises used: gauge_ball, LT.lt.le, mul_comm, le_div_iff₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (ball 0 r) x

Tactic:
gauge_mono (absorbent_ball_zero hr) hs x

Premises used: gauge_mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (ball 0 r) x

Tactic:
exact gauge_mono (absorbent_ball_zero hr) hs x

Premises used: gauge_mono, absorbent_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 (↑r : ℝ) ⊆ s
this : Absorbent.{0, u_2} ℝ (α := E) (ball 0 (↑r : ℝ))
x y : E
⊢ gauge s x = gauge s (y + (x - y))

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 (↑r : ℝ) ⊆ s
this : Absorbent.{0, u_2} ℝ (α := E) (ball 0 (↑r : ℝ))
x y : E
hr₁ : 0 ≤ (↑r : ℝ)
⊢ gauge s y + gauge s (x - y) ≤ gauge s y + ‖x - y‖ / (↑r : ℝ)

Tactic:
grw [gauge_mono this hs (x - y), gauge_ball]

Premises used: HSub.hSub, gauge_ball, gauge_mono
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 (↑r : ℝ) ⊆ s
this : Absorbent.{0, u_2} ℝ (α := E) (ball 0 (↑r : ℝ))
x y : E
⊢ 0 ≤ (↑r : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 (↑r : ℝ) ⊆ s
this : Absorbent.{0, u_2} ℝ (α := E) (ball 0 (↑r : ℝ))
x y : E
rw : gauge s y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * ‖x - y‖
rw₁ : gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖ = gauge s y + (↑r⁻¹ : ℝ) * ‖x - y‖
rw₂ rw₃ : gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖ = gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖
⊢ gauge s y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * dist x y

Tactic:
rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]

Premises used: dist_eq_norm, NNReal.coe_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
h₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ ∃ (K : ℝ≥0), LipschitzWith K (gauge s)

Tactic:
let ⟨r, hr₀, hr⟩ := Metric.mem_nhds_iff.1 h₀
  ⟨(⟨r, hr₀.le⟩ : ℝ≥0)⁻¹, hc.lipschitzWith_gauge hr₀ hr⟩

Premises used: LipschitzWith, gauge, Exists, LT.lt.le, Subtype.mk, _private.0.Convex.lipschitz_gauge.match_1, Inv.inv, Metric.mem_nhds_iff, Exists.intro, Iff.mp, Convex.lipschitzWith_gauge
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
h₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ UniformContinuous (gauge s)

Tactic:
let ⟨_K, hK⟩ := hc.lipschitz_gauge h₀; hK.uniformContinuous

Premises used: UniformContinuous, gauge, LipschitzWith.uniformContinuous, Convex.lipschitz_gauge, _private.0.Convex.uniformContinuous_gauge.match_1
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
rw : gauge (closedBall 0 r) x ≤ gauge s x
⊢ ‖x‖ / r ≤ gauge s x

Tactic:
rw [← gauge_closedBall hr]

Premises used: gauge_closedBall
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x

Tactic:
gauge_mono hs hsr _

Premises used: gauge_mono
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x

Tactic:
exact gauge_mono hs hsr _

Premises used: gauge_mono
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
⊢ gaugeRescale s t x = (gauge s x / gauge t x) • x

Tactic:
rfl

Premises used: gaugeRescale, rfl
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
⊢ gaugeRescale s t 0 = 0

Tactic:
smul_zero _

Premises used: gaugeRescale, smul_zero
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
simp : (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
⊢ gaugeRescale s t (c • x) = c • gaugeRescale s t x

Tactic:
simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]

Premises used: gauge_smul_of_nonneg, gaugeRescale, smul_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
rw : (c / c * (gauge s x / gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
rw₁ : (c / c * c * (gauge s x / gauge t x)) • x = (c * (gauge s x / gauge t x)) • x
rw₂ rw₃ : (c * (gauge s x / gauge t x)) • x = (c * (gauge s x / gauge t x)) • x
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x

Tactic:
rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]

Premises used: div_self_mul_self, mul_right_comm, mul_div_mul_comm
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
rw : gauge t ((gauge s x / gauge t x) • x) = gauge s x
rw₁ : (gauge s x / gauge t x) • gauge t x = gauge s x
rw₂ : gauge s x / gauge t x * gauge t x = gauge s x
rw₃ rw₄ : gauge s x = gauge s x
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
    smul_eq_mul, div_mul_cancel₀ _ hx]

Premises used: div_mul_cancel₀, gauge_smul_of_nonneg, gaugeRescale, gauge_nonneg, div_nonneg, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
pos : ∀ (hx : gauge t x = 0), gauge t (gaugeRescale s t x) ≤ gauge s x
neg : ∀ (hx : ¬gauge t x = 0), gauge t (gaugeRescale s t x) ≤ gauge s x
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
by_cases hx : gauge t x = 0

Premises used: gauge
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
hx : gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
simp [gaugeRescale, hx, gauge_nonneg]

Premises used: gaugeRescale, gauge_nonneg
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
(gauge_gaugeRescale' s hx).le

Premises used: Eq.le, gauge_gaugeRescale'
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
exact (gauge_gaugeRescale' s hx).le

Premises used: Eq.le, gauge_gaugeRescale'
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
inl : gaugeRescale s s 0 = 0
inr : ∀ (hx : x ≠ 0), gaugeRescale s s x = x
⊢ gaugeRescale s s x = x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
inr : gauge s x ≠ 0
⊢ gaugeRescale s s x = x

Tactic:
rw [gaugeRescale, div_self, one_smul]

Premises used: gaugeRescale, one_smul, div_self
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gauge s x ≠ 0

Tactic:
((gauge_pos hsa hsb).2 hx).ne'

Premises used: Iff.mpr, gauge_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gauge s x ≠ 0

Tactic:
exact ((gauge_pos hsa hsb).2 hx).ne'

Premises used: Iff.mpr, gauge_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s = id

Tactic:
funext <| gaugeRescale_self_apply hsa hsb

Premises used: gaugeRescale_self_apply, funext
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
inl : gauge t (gaugeRescale s t 0) = gauge s 0
inr : ∀ (hx : x ≠ 0), gauge t (gaugeRescale s t x) = gauge s x
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gauge t (gaugeRescale s t 0) = gauge s 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
gauge_gaugeRescale' s ((gauge_pos hta htb).2 hx).ne'

Premises used: Iff.mpr, gauge_pos, LT.lt.ne', gauge_gaugeRescale'
-- Module: Mathlib.Analysis.Convex.GaugeRescale
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
exact gauge_gaugeRescale' s ((gauge_pos hta htb).2 hx).ne'

Premises used: Iff.mpr, gauge_pos, LT.lt.ne', gauge_gaugeRescale'