awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
h :
  ∀ (r : ℝ) (h₁ : Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ r⁻¹ • x) ⁻¹' s) r)
    (h₂ : Membership.mem (γ := Set ℝ) (Ioo 0 1) r), x ∈ r • s ∧ 0 < r ∧ r < 1
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂

Premises used: mem_interior_iff_mem_nhds, Ioo_mem_nhdsLT, Iff.mp, one_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
r : ℝ
h₁ : Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ r⁻¹ • x) ⁻¹' s) r
h₂ : Membership.mem (γ := Set ℝ) (Ioo 0 1) r
⊢ x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩

Premises used: Iff.mpr, LT.lt.ne', And.left, And.intro, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
r : ℝ
h₁ : Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ r⁻¹ • x) ⁻¹' s) r
h₂ : Membership.mem (γ := Set ℝ) (Ioo 0 1) r
⊢ x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
have H₂ : ∀ᶠ r in 𝓝[<] (1 : ℝ), x ∈ r • s ∧ 0 < r ∧ r < 1 := by
    filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂
    exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
rcases : ∀ (r : ℝ) (hxr : x ∈ r • s) (hr₀ : 0 < r) (hr₁ : r < 1), Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x

Tactic:
rcases H₂.exists with ⟨r, hxr, hr₀, hr₁⟩

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
r : ℝ
hxr : x ∈ r • s
hr₀ : 0 < r
hr₁ : r < 1
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x

Tactic:
(gauge_le_of_mem hr₀.le hxr).trans_lt hr₁

Premises used: gauge_le_of_mem, Set.Mem, setOf, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
r : ℝ
hxr : x ∈ r • s
hr₀ : 0 < r
hr₁ : r < 1
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x

Tactic:
exact (gauge_le_of_mem hr₀.le hxr).trans_lt hr₁

Premises used: gauge_le_of_mem, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ {x : E | gauge s x < 1} = s

Tactic:
(gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm ?_

Premises used: absorbent_nhds_zero, gauge_lt_one_subset_self, HasSubset.Subset.antisymm, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
refine : s ⊆ {x : E | gauge s x < 1}
⊢ {x : E | gauge s x < 1} = s

Tactic:
refine (gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm ?_

Premises used: absorbent_nhds_zero, gauge_lt_one_subset_self, HasSubset.Subset.antisymm, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ interior s ⊆ {x : E | gauge s x < 1}

Tactic:
interior_subset_gauge_lt_one s

Premises used: interior_subset_gauge_lt_one
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
h : s = interior s
⊢ s ⊆ {x : E | gauge s x < 1}

Tactic:
convert! interior_subset_gauge_lt_one s

Premises used: interior_subset_gauge_lt_one
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ s = interior s

Tactic:
hs₂.interior_eq.symm

Premises used: IsOpen.interior_eq, Eq.symm
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ s = interior s

Tactic:
exact hs₂.interior_eq.symm

Premises used: IsOpen.interior_eq, Eq.symm
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₂ : IsOpen[inst_2] s
x : E
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ x ∈ interior s

Tactic:
rwa [hs₂.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
rwa rwa₁ rwa₂ rwa₃ : x ∈ ε • s
⊢ ε⁻¹ • x ∈ s

Tactic:
rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']

Premises used: LT.lt.ne', Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
⊢ ε⁻¹ • x ∈ s

Tactic:
have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s (ε⁻¹ • x) < 1

Tactic:
have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
rwa : ∀ (h_gauge_lt : ε⁻¹ • gauge s x < 1), gauge s x < ε
rwa₁ : ∀ (h_gauge_lt : ε⁻¹ * gauge s x < 1), gauge s x < ε
rwa₂ : ∀ (h_gauge_lt : gauge s x < ε * 1), gauge s x < ε
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h_gauge_lt : gauge s x < ε), gauge s x < ε
⊢ gauge s x < ε

Tactic:
rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt

Premises used: Iff.mpr, gauge_smul_of_nonneg, inv_mul_lt_iff₀, LT.lt.le, inv_nonneg, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
h₁ : ∀ (hr₀ : 0 ≤ r) (hr₁ : r < 1), r • x ∈ s
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) r → r • x ∈ s

Tactic:
⟨hr₀, hr₁⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
h₁ : ∀ (r : ℝ) (hr₀ : 0 ≤ r) (hr₁ : r < 1), r • x ∈ s
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s

Tactic:
filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩

Premises used: Ico_mem_nhdsLT, one_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
h₁ : Membership.mem (γ := Set E) {x : E | gauge s x < 1} (r • x)
⊢ r • x ∈ s

Tactic:
apply gauge_lt_one_subset_self hc hs₀ ha

Premises used: gauge_lt_one_subset_self
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
h₁ : r • gauge s x < 1
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} (r • x)

Tactic:
rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]

Premises used: gauge_smul_of_nonneg, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • gauge s x < 1

Tactic:
mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h

Premises used: mul_lt_one_of_nonneg_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • gauge s x < 1

Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h

Premises used: mul_lt_one_of_nonneg_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s

Tactic:
have : ∀ᶠ r : ℝ in 𝓝[<] 1, r • x ∈ s := by
    filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩
    apply gauge_lt_one_subset_self hc hs₀ ha
    rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]
    exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ x ∈ closure[inst_2] s

Tactic:
mem_closure_of_tendsto ?_ this

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
refine : Tendsto (fun (x_1 : ℝ) ↦ x_1 • x) (𝓝[<] 1) (𝓝 x)
⊢ x ∈ closure[inst_2] s

Tactic:
refine mem_closure_of_tendsto ?_ this

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Continuous[_, inst_2] fun (x_1 : ℝ) ↦ x_1 • x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Tendsto (fun (x_1 : ℝ) ↦ x_1 • x) (𝓝[<] 1) (𝓝 x)

Tactic:
exact Filter.Tendsto.mono_left (Continuous.tendsto' (by fun_prop) _ _ (one_smul _ _))
    inf_le_left

Premises used: one_smul, Filter.Tendsto.mono_left, inf_le_left, Continuous.tendsto'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x = 1
⊢ x ∈ frontier s

Tactic:
⟨mem_closure_of_gauge_le_one hc hs₀ ha h.le, fun h' ↦
    (interior_subset_gauge_lt_one s h').out.ne h⟩

Premises used: frontier, Membership.mem.out, Set.Mem, Set.diff, setOf, interior_subset_gauge_lt_one, Eq.le, And.intro, mem_closure_of_gauge_le_one, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Tactic:
nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, nhdsGE_basis_Icc, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
refine : ∀ (ε : ℝ) (hε : 0 < ε), ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Tactic:
refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_

Premises used: Iff.mpr, nhdsGE_basis_Icc, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
ε : ℝ
hε : 0 < ε
⊢ Membership.mem (γ := Filter E) (𝓝 0) (ε • s)

Tactic:
rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs

Premises used: set_smul_mem_nhds_zero_iff, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
ε : ℝ
hε : 0 < ε
hs₁ : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
⊢ 0 < ε

Tactic:
rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs

Premises used: set_smul_mem_nhds_zero_iff, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
ε : ℝ
hs : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
hε : 0 < ε
h : ∀ (x : E) (hx : x ∈ ε • s), gauge s x ∈ Icc 0 ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Tactic:
filter_upwards [hs] with x hx
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
ε : ℝ
hs : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
hε : 0 < ε
x : E
hx : x ∈ ε • s
⊢ gauge s x ∈ Icc 0 ε

Tactic:
⟨gauge_nonneg _, gauge_le_of_mem hε.le hx⟩

Premises used: gauge_le_of_mem, Set.Mem, setOf, LT.lt.le, Set.Icc, gauge_nonneg, And.intro
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
ε : ℝ
hs : Membership.mem (γ := Filter E) (𝓝 0) (ε • s)
hε : 0 < ε
x : E
hx : x ∈ ε • s
⊢ gauge s x ∈ Icc 0 ε

Tactic:
exact ⟨gauge_nonneg _, gauge_le_of_mem hε.le hx⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Tendsto (gauge s) (𝓝 0) (𝓝 0)

Tactic:
(tendsto_gauge_nhds_zero_nhdsGE hs).mono_right inf_le_left

Premises used: tendsto_gauge_nhds_zero_nhdsGE, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
rw : Tendsto (gauge s) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (gauge s) 0

Tactic:
rw [ContinuousAt, gauge_zero]

Premises used: ContinuousAt, gauge_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Tendsto (gauge s) (𝓝 0) (𝓝 0)

Tactic:
tendsto_gauge_nhds_zero hs

Premises used: tendsto_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Tendsto (gauge s) (𝓝 0) (𝓝 0)

Tactic:
exact tendsto_gauge_nhds_zero hs

Premises used: tendsto_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hb : Bornology.IsVonNBounded ℝ s
h₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ comap (gauge s) (𝓝 0) = 𝓝 0

Tactic:
(comap_gauge_nhds_zero_le (absorbent_nhds_zero h₀) hb).antisymm
    (tendsto_gauge_nhds_zero h₀).le_comap

Premises used: comap_gauge_nhds_zero_le, Filter.Tendsto.le_comap, absorbent_nhds_zero, LE.le.antisymm, tendsto_gauge_nhds_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Absorbent ℝ s

Tactic:
have ha : Absorbent ℝ s := absorbent_nhds_zero hs₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
⊢ ContinuousAt (gauge s) x

Tactic:
(nhds_basis_Icc_pos _).tendsto_right_iff.2 fun ε hε₀ ↦ ?_

Premises used: Iff.mpr, nhds_basis_Icc_pos, ContinuousAt, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
refine : ∀ (ε : ℝ) (hε₀ : 0 < ε), ∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)
⊢ ContinuousAt (gauge s) x

Tactic:
refine (nhds_basis_Icc_pos _).tendsto_right_iff.2 fun ε hε₀ ↦ ?_

Premises used: Iff.mpr, nhds_basis_Icc_pos, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
rw : ∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)

Tactic:
rw [← map_add_left_nhds_zero, eventually_map]

Premises used: Filter.eventually_map, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
⊢ Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))

Tactic:
have : ε • s ∩ -(ε • s) ∈ 𝓝 0 :=
    inter_mem ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀)
      (neg_mem_nhds_zero _ ((set_smul_mem_nhds_zero_iff hε₀.ne').2 hs₀))
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
h : ∀ (y : E) (hy : y ∈ ε • s ∩ -(ε • s)), gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
⊢ ∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
h : gauge s x - ε ≤ gauge s (x + y)
h₁ : gauge s (x + y) ≤ gauge s x + ε
⊢ gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
h : gauge s x ≤ gauge s (x + y) + ε
⊢ gauge s x - ε ≤ gauge s (x + y)

Tactic:
rw [sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x = gauge s (x + y + -y)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s (x + y + -y) ≤ gauge s (x + y) + gauge s (-y)

Tactic:
gauge_add_le hc ha _ _

Premises used: gauge_add_le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : Membership.mem (γ := Filter E) (𝓝 0) (ε • s ∩ -(ε • s))
y : E
hy : y ∈ ε • s ∩ -(ε • s)
grw grw₁ : gauge s (x + y) + ε ≤ gauge s (x + y) + ε
⊢ gauge s (x + y) + gauge s (-y) ≤ gauge s (x + y) + ε

Tactic:
grw [gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)]

Premises used: Set.mem_neg, gauge_le_of_mem, LT.lt.le, And.right, Iff.mp