awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
inl : gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0
inr : ∀ (hx : x ≠ 0), gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u 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 u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
⊢ gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 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 u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
inr : gauge t x ≠ 0
inr₁ : 0 ≤ gauge s x / gauge t x
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul,
    div_mul_div_cancel₀]

Premises used: gaugeRescale, smul_smul, gaugeRescale_def, gaugeRescale_smul, div_mul_div_cancel₀
-- 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 u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t x ≠ 0

Tactic:
((gauge_pos hta htb).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 t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ 0 ≤ gauge s x / gauge t x

Tactic:
div_nonneg (gauge_nonneg _) (gauge_nonneg _)

Premises used: gauge_nonneg, div_nonneg
-- 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 u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ≠ 0
⊢ gauge t x ≠ 0

Tactic:
exacts [((gauge_pos hta htb).2 hx).ne', div_nonneg (gauge_nonneg _) (gauge_nonneg _)]

Premises used: Iff.mpr, gauge_pos, LT.lt.ne', gauge_nonneg, div_nonneg
-- 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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hsa₁ : Absorbent ℝ s
hsb₁ : IsVonNBounded ℝ s
hta₁ : Absorbent ℝ t
htb₁ : IsVonNBounded ℝ t
⊢ gaugeRescale t s (gaugeRescale s t x) = x

Tactic:
rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply]

Premises used: gaugeRescale_self_apply, gaugeRescale_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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ Absorbent ℝ s

Tactic:
assumption
-- 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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ IsVonNBounded ℝ s

Tactic:
assumption
-- 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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ Absorbent ℝ t

Tactic:
assumption
-- 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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ IsVonNBounded ℝ t

Tactic:
assumption
-- 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
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
hsa₁ : Absorbent ℝ t
hsb₁ : IsVonNBounded ℝ t
hta₁ : Absorbent ℝ s
htb₁ : IsVonNBounded ℝ s
⊢ gaugeRescale s t (gaugeRescale t s x) = x

Tactic:
rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply]

Premises used: gaugeRescale_self_apply, gaugeRescale_gaugeRescale
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
rw : gauge t (gaugeRescale s t x) < 1
hc₁ : Convex ℝ t
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) t
⊢ gaugeRescale s t x ∈ interior t

Tactic:
rw [← gauge_lt_one_iff_mem_interior]

Premises used: gauge_lt_one_iff_mem_interior
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ Convex ℝ t

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ Convex ℝ t

Tactic:
try assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
try assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ gauge t (gaugeRescale s t x) < 1

Tactic:
(gauge_gaugeRescale_le _ _ _).trans_lt (interior_subset_gauge_lt_one _ hx)

Premises used: interior_subset_gauge_lt_one, gauge_gaugeRescale_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ gauge t (gaugeRescale s t x) < 1

Tactic:
exact (gauge_gaugeRescale_le _ _ _).trans_lt (interior_subset_gauge_lt_one _ hx)

Premises used: interior_subset_gauge_lt_one, gauge_gaugeRescale_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
hsc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
htc : Convex ℝ t
ht₀ : 0 ∈ t
hta : Absorbent ℝ t
⊢ MapsTo (gaugeRescale s t) (closure[inst_2] s) (closure[inst_2] t)

Tactic:
fun _x hx ↦
  mem_closure_of_gauge_le_one htc ht₀ hta <| (gauge_gaugeRescale_le _ _ _).trans <|
    (gauge_le_one_iff_mem_closure hsc hs₀).2 hx

Premises used: Iff.mpr, Set.MapsTo, gauge_le_one_iff_mem_closure, gauge_gaugeRescale_le, mem_closure_of_gauge_le_one, LE.le.trans
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
⊢ Absorbent ℝ t

Tactic:
have hta : Absorbent ℝ t := absorbent_nhds_zero ht₀
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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)

Tactic:
continuous_iff_continuousAt.2 fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
refine : ∀ (x : E), ContinuousAt (gaugeRescale s t) x
⊢ Continuous[inst_2, inst_2] (gaugeRescale s t)

Tactic:
refine continuous_iff_continuousAt.2 fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
inr : ∀ (hx : x ≠ 0), ContinuousAt (gaugeRescale s t) x
⊢ ContinuousAt (gaugeRescale s t) 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 : 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
inl : Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (gaugeRescale s t) 0

Tactic:
rw [ContinuousAt, gaugeRescale_zero]

Premises used: ContinuousAt, gaugeRescale_zero
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
inl : Tendsto (gaugeRescale s t) (𝓝 0) (comap (gauge t) (𝓝 0))
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 0)

Tactic:
nth_rewrite 2 [← comap_gauge_nhds_zero htb ht₀]

Premises used: comap_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
inl : Tendsto (β := ℝ) (fun (x : E) ↦ gauge s x) (𝓝 0) (𝓝 0)
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (comap (gauge t) (𝓝 0))

Tactic:
simp only [tendsto_comap_iff, Function.comp_def, gauge_gaugeRescale _ hta htb]

Premises used: gauge_gaugeRescale, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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 (β := ℝ) (fun (x : E) ↦ gauge s x) (𝓝 0) (𝓝 0)

Tactic:
tendsto_gauge_nhds_zero hs₀

Premises used: tendsto_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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 (β := ℝ) (fun (x : E) ↦ gauge s x) (𝓝 0) (𝓝 0)

Tactic:
exact tendsto_gauge_nhds_zero hs₀

Premises used: tendsto_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
hx : x ≠ 0
⊢ ContinuousAt (gaugeRescale s t) x

Tactic:
((continuousAt_gauge hs hs₀).div (continuousAt_gauge ht ht₀)
      ((gauge_pos hta htb).2 hx).ne').smul continuousAt_id

Premises used: Iff.mpr, gaugeRescale, ContinuousAt.smul, gauge_pos, continuousAt_gauge, LT.lt.ne', ContinuousAt.div, continuousAt_id
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
hx : x ≠ 0
⊢ ContinuousAt (gaugeRescale s t) x

Tactic:
exact ((continuousAt_gauge hs hs₀).div (continuousAt_gauge ht ht₀)
      ((gauge_pos hta htb).2 hx).ne').smul continuousAt_id

Premises used: Iff.mpr, ContinuousAt.smul, gauge_pos, continuousAt_gauge, LT.lt.ne', ContinuousAt.div, continuousAt_id
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
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] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).toFun

Tactic:
apply continuous_gaugeRescale

Premises used: continuous_gaugeRescale
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ Convex ℝ s

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ Membership.mem (γ := Filter E) (𝓝 0) s

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ Convex ℝ t

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ IsVonNBounded ℝ t

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
hs : Convex ℝ t
hs₁ : Membership.mem (γ := Filter E) (𝓝 0) t
ht : Convex ℝ s
ht₁ : Membership.mem (γ := Filter E) (𝓝 0) s
htb₁ : IsVonNBounded ℝ s
⊢ Continuous[inst_2, inst_2] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).invFun

Tactic:
apply continuous_gaugeRescale

Premises used: continuous_gaugeRescale
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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_1 t_1 : Set 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
⊢ IsVonNBounded ℝ s

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
rw : (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm : (a : E) → E) '' interior t ⊆ interior s
⊢ interior t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' interior s

Tactic:
rw [← Homeomorph.preimage_symm, ← image_subset_iff]

Premises used: Homeomorph.preimage_symm, Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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).symm : (a : E) → E) '' interior t ⊆ interior s

Tactic:
(mapsTo_gaugeRescale_interior hs₀ hsc).image_subset

Premises used: gaugeRescale, mapsTo_gaugeRescale_interior, Set.MapsTo.image_subset
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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).symm : (a : E) → E) '' interior t ⊆ interior s

Tactic:
exact (mapsTo_gaugeRescale_interior hs₀ hsc).image_subset

Premises used: mapsTo_gaugeRescale_interior, Set.MapsTo.image_subset
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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

Tactic:
Subset.antisymm (mapsTo_gaugeRescale_closure hsc hs₀ htc
    (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_

Premises used: Set.Subset.antisymm, mapsTo_gaugeRescale_closure, absorbent_nhds_zero, mem_of_mem_nhds, Set.MapsTo.image_subset
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
refine : closure[inst_2] t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s
⊢ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s = closure[inst_2] t

Tactic:
refine Subset.antisymm (mapsTo_gaugeRescale_closure hsc hs₀ htc
    (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_

Premises used: Set.Subset.antisymm, mapsTo_gaugeRescale_closure, absorbent_nhds_zero, mem_of_mem_nhds, Set.MapsTo.image_subset
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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
rw : (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm : (a : E) → E) '' closure[inst_2] t ⊆ closure[inst_2] s
⊢ closure[inst_2] t ⊆ (⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) : (a : E) → E) '' closure[inst_2] s

Tactic:
rw [← Homeomorph.preimage_symm, ← image_subset_iff]

Premises used: Homeomorph.preimage_symm, Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.GaugeRescale
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).symm : (a : E) → E) '' closure[inst_2] t ⊆ closure[inst_2] s

Tactic:
(mapsTo_gaugeRescale_closure htc ht₀ hsc
    (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀)).image_subset

Premises used: gaugeRescale, mapsTo_gaugeRescale_closure, absorbent_nhds_zero, mem_of_mem_nhds, Set.MapsTo.image_subset