awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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)
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
have inr : ∀ (hx : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
have h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} (Ioi 0)
Tactic: convert! csInf_Ioi (a := (0 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : 0 < ‖x‖
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)}) (0 x)
have h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ ‖x‖ = 0)} ∅
Tactic: convert! Real.sInf_empty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ gauge (closedBall 0 r) x = ‖x‖ / r
have inl : ∀ (hr : LE.le (α := ℝ) 0 0), gauge (closedBall 0 0) x = ‖x‖ / 0
Tactic: rcases hr.eq_or_lt with rfl | hr'
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (closedBall 0 r) x = ‖x‖ / r
have inr : ∀ (hr' : 0 < r), gauge (closedBall 0 r) x = ‖x‖ / r
Tactic: rcases hr.eq_or_lt with rfl | hr'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hr : LE.le (α := ℝ) 0 0
⊢ gauge (closedBall 0 0) x = ‖x‖ / 0
have inl : Eq (α := ℝ) (0 x) 0
Tactic: rw [div_zero, closedBall_zero', singleton_zero, gauge_closure_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 = ‖x‖ / r
have inr : gauge (closedBall 0 r) x ≤ ‖x‖ / r
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (closedBall 0 r) x = ‖x‖ / r
have inr₁ : ‖x‖ / r ≤ gauge (closedBall 0 r) x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 ≤ ‖x‖ / r
have inr : gauge (closedBall 0 r) x ≤ gauge (ball 0 r) x
Tactic: rw [← gauge_ball hr]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
have refine : Filter.Tendsto (HDiv.hDiv ‖x‖) (𝓝[>] r) (𝓝 (‖x‖ / r))
Tactic: refine le_of_tendsto ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ ‖x‖ / r ≤ gauge (closedBall 0 r) x
have inr : ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖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'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ ∀ᶠ (R : ℝ) in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
have h : ∀ (R : ℝ) (hR : R ∈ Ioi r), ‖x‖ / R ≤ gauge (closedBall 0 r) x
Tactic: filter_upwards [self_mem_nhdsWithin] with R hR
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ ‖x‖ / R ≤ gauge (closedBall 0 r) x
have h : gauge (ball 0 R) x ≤ gauge (closedBall 0 r) x
Tactic: rw [← gauge_ball (hr.trans hR.out.le)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
have h : Absorbent.{0, u_2} ℝ (α := E) (closedBall 0 r)
Tactic: refine gauge_mono ?_ (closedBall_subset_ball hR) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
⊢ r * gauge s x ≤ ‖x‖
have inl : ∀ (hr : r ≤ 0), r * gauge s x ≤ ‖x‖
Tactic: obtain hr | hr := le_or_gt r 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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‖
⊢ r * gauge s x ≤ ‖x‖
have inr : ∀ (hr : 0 < r), r * gauge s x ≤ ‖x‖
Tactic: obtain hr | hr := le_or_gt r 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ r * gauge s x ≤ ‖x‖
have inr : gauge s x ≤ gauge (ball 0 r) x
Tactic: rw [mul_comm, ← le_div_iff₀ hr, ← gauge_ball hr.le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 y + gauge s (x - y) ≤ gauge s y + ‖x - y‖ / (↑r : ℝ)
have hr₁ : 0 ≤ (↑r : ℝ)
Tactic: grw [gauge_mono this hs (x - y), gauge_ball]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * dist x y
have rw : gauge s y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * ‖x - y‖
Tactic: rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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‖
⊢ gauge s y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * dist x y
have rw₁ : gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖ = gauge s y + (↑r⁻¹ : ℝ) * ‖x - y‖
Tactic: rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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‖
⊢ gauge s y + ‖x - y‖ / (↑r : ℝ) = gauge s y + (↑r⁻¹ : ℝ) * dist x y
have rw₂ : gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖ = gauge s y + (↑r : ℝ)⁻¹ * ‖x - y‖
Tactic: rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ ‖x‖ / r ≤ gauge s x
have rw : gauge (closedBall 0 r) x ≤ gauge s x
Tactic: rw [← gauge_closedBall hr]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ gaugeRescale s t (c • x) = c • gaugeRescale s t x
have simp : (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
Tactic: simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
have rw : (c / c * (gauge s x / 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
have rw₁ : (c / c * c * (gauge s x / gauge t x)) • x = (c * (gauge s x / gauge t x)) • x
Tactic: rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
have rw₂ : (c * (gauge s x / gauge t x)) • x = (c * (gauge s x / gauge t x)) • x
Tactic: rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
have rw : gauge t ((gauge s x / gauge t x) • x) = gauge s x
Tactic: rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
    smul_eq_mul, div_mul_cancel₀ _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) = gauge s x
have rw₁ : (gauge s x / gauge t x) • gauge 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) = gauge s x
have rw₂ : gauge s x / gauge t x * gauge 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) = gauge s x
have rw₃ : gauge s x = gauge s x
Tactic: rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
    smul_eq_mul, div_mul_cancel₀ _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
x : E
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x
have pos : ∀ (hx : gauge t x = 0), gauge t (gaugeRescale s t x) ≤ gauge s x
Tactic: by_cases hx : gauge t x = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x
have neg : ∀ (hx : ¬gauge t x = 0), gauge t (gaugeRescale s t x) ≤ gauge s x
Tactic: by_cases hx : gauge t x = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gaugeRescale s s x = x
have inl : gaugeRescale s s 0 = 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gaugeRescale s s x = x
have inr : ∀ (hx : x ≠ 0), gaugeRescale s s x = x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gaugeRescale s s x = x
have inr : gauge s x ≠ 0
Tactic: rw [gaugeRescale, div_self, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) = gauge s x
have inl : gauge t (gaugeRescale s t 0) = gauge s 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
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
⊢ gauge t (gaugeRescale s t x) = gauge s x
have inr : ∀ (hx : x ≠ 0), gauge t (gaugeRescale s t x) = gauge s x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
have inl : gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
inl : gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
have inr : ∀ (hx : x ≠ 0), gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
have inr : gauge t x ≠ 0
Tactic: rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul,
    div_mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
inr : gauge t x ≠ 0
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
have inr₁ : 0 ≤ gauge s x / gauge t x
Tactic: rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul,
    div_mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s t : Set E
h₀ : Membership.mem (γ := Filter E) (𝓝 0) t
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gaugeRescale s t x ∈ interior t
have rw : gauge t (gaugeRescale s t x) < 1
Tactic: rw [← gauge_lt_one_iff_mem_interior]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
⊢ Continuous[inst_2, inst_2] (gaugeRescale s t)
have hta : Absorbent ℝ t
Tactic: have hta : Absorbent ℝ t := absorbent_nhds_zero ht₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Continuous[inst_2, inst_2] (gaugeRescale s t)
have refine : ∀ (x : E), ContinuousAt (gaugeRescale s t) x
Tactic: refine continuous_iff_continuousAt.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
x : E
⊢ ContinuousAt (gaugeRescale s t) x
have inl : ContinuousAt (gaugeRescale s t) 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
x : E
inl : ContinuousAt (gaugeRescale s t) 0
⊢ ContinuousAt (gaugeRescale s t) x
have inr : ∀ (hx : x ≠ 0), ContinuousAt (gaugeRescale s t) x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ ContinuousAt (gaugeRescale s t) 0
have inl : Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 0)
Tactic: rw [ContinuousAt, gaugeRescale_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 0)
have inl : Tendsto (gaugeRescale s t) (𝓝 0) (comap (gauge t) (𝓝 0))
Tactic: nth_rewrite 2 [← comap_gauge_nhds_zero htb ht₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ht : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (comap (gauge t) (𝓝 0))
have inl : Tendsto (β := ℝ) (fun (x : E) ↦ gauge s x) (𝓝 0) (𝓝 0)
Tactic: simp only [tendsto_comap_iff, Function.comp_def, gauge_gaugeRescale _ hta htb]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
⊢ interior t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' interior s
have rw : (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm : (a : E) → E) '' interior t ⊆ interior s
Tactic: rw [← Homeomorph.preimage_symm, ← image_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
⊢ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t
have refine : closure[inst_2] t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s
Tactic: refine Subset.antisymm (mapsTo_gaugeRescale_closure hsc hs₀ htc
    (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : Membership.mem (γ := Filter E) (𝓝 0) t
htb : IsVonNBounded ℝ t
⊢ closure[inst_2] t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s
have rw : (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm : (a : E) → E) '' closure[inst_2] t ⊆ closure[inst_2] s
Tactic: rw [← Homeomorph.preimage_symm, ← image_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
⊢ ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧
      (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t
have rsuffices : ∀ (e : E ≃ₜ E) (h₁ : (⇑e : (a : E) → E) '' interior s = interior t)
  (h₂ : (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t),
  ∃ (e : E ≃ₜ E),
    (⇑e : (a : E) → E) '' interior s = interior t ∧
      (⇑e : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t ∧ (⇑e : (a : E) → E) '' frontier s = frontier t
Tactic: rsuffices ⟨e, h₁, h₂⟩ : ∃ e : E ≃ₜ E, e '' interior s = interior t ∧ e '' closure s = closure t