awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : _root_.gauge s x = _root_.gauge s (x + y + -y)
gauge₁ : _root_.gauge s (x + y) + _root_.gauge s (-y) ≤ _root_.gauge s (x + y) + ε
⊢ _root_.gauge s x ≤ _root_.gauge s (x + y) + ε

Tactic:
calc
      gauge s x = gauge s (x + y + (-y)) := by simp
      _ ≤ gauge s (x + y) + gauge s (-y) := gauge_add_le hc ha _ _
      _ ≤ gauge s (x + y) + ε := by grw [gauge_le_of_mem hε₀.le (mem_neg.1 hy.2)]

Premises used: gauge, HAdd.hAdd, gauge_add_le, Neg.neg
-- 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) ≤ gauge s x + 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 + ε ≤ gauge s x + ε
⊢ gauge s x + gauge s y ≤ gauge s x + ε

Tactic:
grw [gauge_le_of_mem hε₀.le hy.1]

Premises used: gauge_le_of_mem, LT.lt.le, And.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 : 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 : _root_.gauge s x + _root_.gauge s y ≤ _root_.gauge s x + ε
⊢ _root_.gauge s (x + y) ≤ _root_.gauge s x + ε

Tactic:
calc
      gauge s (x + y) ≤ gauge s x + gauge s y := gauge_add_le hc ha _ _
      _ ≤ gauge s x + ε := by grw [gauge_le_of_mem hε₀.le hy.1]

Premises used: gauge, HAdd.hAdd, gauge_add_le
-- 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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Continuous[inst_2, _] (gauge s)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ continuousAt_gauge hc hs₀

Premises used: Iff.mpr, continuousAt_gauge, continuous_iff_continuousAt
-- 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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ {x : E | gauge s x < 1} = interior s

Tactic:
Subset.antisymm (fun x hx ↦ ?_) (interior_subset_gauge_lt_one s)

Premises used: Set.Subset.antisymm, 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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x), x ∈ interior s
⊢ {x : E | gauge s x < 1} = interior s

Tactic:
refine Subset.antisymm (fun x hx ↦ ?_) (interior_subset_gauge_lt_one s)

Premises used: Set.Subset.antisymm, 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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
x : E
hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
rcases : ∀ (y : E) (hys : y ∈ s) (hxy : x ∈ openSegment ℝ 0 y), x ∈ interior s
⊢ x ∈ interior s

Tactic:
rcases mem_openSegment_of_gauge_lt_one (absorbent_nhds_zero hs₀) hx with ⟨y, hys, hxy⟩

Premises used: absorbent_nhds_zero, mem_openSegment_of_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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
x : E
hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
y : E
hys : y ∈ s
hxy : x ∈ openSegment ℝ 0 y
⊢ x ∈ interior s

Tactic:
hc.openSegment_interior_self_subset_interior (mem_interior_iff_mem_nhds.2 hs₀) hys hxy

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Convex.openSegment_interior_self_subset_interior
-- 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 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : Membership.mem (γ := Filter E) (𝓝 0) s
x : E
hx : Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
y : E
hys : y ∈ s
hxy : x ∈ openSegment ℝ 0 y
⊢ x ∈ interior s

Tactic:
exact hc.openSegment_interior_self_subset_interior (mem_interior_iff_mem_nhds.2 hs₀) hys hxy

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Convex.openSegment_interior_self_subset_interior
-- 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
⊢ gauge s x < 1 ↔ x ∈ interior s

Tactic:
Set.ext_iff.1 (gauge_lt_one_eq_interior hc hs₀) _

Premises used: Set.Mem, gauge_lt_one_eq_interior, Iff.mp, Set.ext_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
⊢ gauge s x ≤ 1 ↔ x ∈ closure[inst_2] s

Tactic:
⟨mem_closure_of_gauge_le_one hc (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀), fun h ↦
    le_on_closure (fun _ ↦ gauge_le_one_of_mem) (continuous_gauge hc hs₀).continuousOn
      continuousOn_const h⟩

Premises used: gauge_le_one_of_mem, Continuous.continuousOn, continuousOn_const, absorbent_nhds_zero, continuous_gauge, mem_of_mem_nhds, Iff.intro, mem_closure_of_gauge_le_one, le_on_closure
-- 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
rw : x ∈ closure[inst_2] s ∧ x ∉ interior s ↔ x ∈ frontier s
⊢ gauge s x = 1 ↔ x ∈ frontier s

Tactic:
rw [eq_iff_le_not_lt, gauge_le_one_iff_mem_closure hc hs₀, gauge_lt_one_iff_mem_interior hc hs₀]

Premises used: eq_iff_le_not_lt, gauge_le_one_iff_mem_closure, gauge_lt_one_iff_mem_interior
-- 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
⊢ x ∈ closure[inst_2] s ∧ x ∉ interior s ↔ x ∈ frontier s

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst_5 : TopologicalSpace E
inst_6 : ContinuousSMul ℝ E
hs : IsOpen[inst_5] s
x : E
hx : x ∈ s
⊢ LT.lt (α := ℝ) ((gaugeSeminorm (s := s) hs₀ hs₁ hs₂ : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
gauge_lt_one_of_mem_of_isOpen hs hx

Premises used: gauge_lt_one_of_mem_of_isOpen, gauge
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst_5 : TopologicalSpace E
inst_6 : ContinuousSMul ℝ E
hs : IsOpen[inst_5] s
rw : {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := s) hs₀ hs₁ hs₂ : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = s
⊢ (gaugeSeminorm (s := s) hs₀ hs₁ hs₂).ball 0 1 = s

Tactic:
rw [Seminorm.ball_zero_eq]

Premises used: Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst_5 : TopologicalSpace E
inst_6 : ContinuousSMul ℝ E
hs : IsOpen[inst_5] s
⊢ {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := s) hs₀ hs₁ hs₂ : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = s

Tactic:
gauge_lt_one_eq_self_of_isOpen hs₁ hs₂.zero_mem hs

Premises used: gauge_lt_one_eq_self_of_isOpen, gauge, Absorbent.zero_mem, setOf
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst_5 : TopologicalSpace E
inst_6 : ContinuousSMul ℝ E
hs : IsOpen[inst_5] s
⊢ {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := s) hs₀ hs₁ hs₂ : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = s

Tactic:
exact gauge_lt_one_eq_self_of_isOpen hs₁ hs₂.zero_mem hs

Premises used: gauge_lt_one_eq_self_of_isOpen, Absorbent.zero_mem
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
h : ∀ (x : E), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
⊢ gauge (p.ball 0 1) = (⇑p : (a : E) → ℝ)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
h : ∀ (hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
h₁ : ∀ (hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}), gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x

Tactic:
obtain hp | hp := { r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1 }.eq_empty_or_nonempty

Premises used: setOf, Membership.mem, Set.eq_empty_or_nonempty, And, Seminorm.ball, LT.lt, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x

Tactic:
rw [gauge, hp, Real.sInf_empty]

Premises used: gauge, Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ∀ (h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)), False
⊢ Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
have hpx : 0 < p x := (apply_nonneg _ _).lt_of_ne h
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ False

Tactic:
hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩

Premises used: HMul.hMul, Set.Mem, smul_inv_smul₀, Eq.subset, LT.lt.ne', Inv.inv, And.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
h₁ : (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ))⁻¹ • x ∈ p.ball 0 1
⊢ False

Tactic:
refine hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩

Premises used: HMul.hMul, smul_inv_smul₀, Eq.subset, LT.lt.ne', Inv.inv, And.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
h₁ : (p : (a : E) → ℝ) x < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ))⁻¹ • x ∈ p.ball 0 1

Tactic:
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpx₂),
      inv_mul_lt_iff₀ hpx₂, mul_one]

Premises used: Iff.mpr, Seminorm.mem_ball_zero, inv_mul_lt_iff₀, inv_pos, SeminormClass.map_smul_eq_mul, abs_of_pos, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ (p : (a : E) → ℝ) x < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
lt_mul_of_one_lt_left hpx one_lt_two

Premises used: one_lt_two, lt_mul_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Eq (α := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} ∅
h : ¬Eq (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx : LT.lt (α := ℝ) (0 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
hpx₂ : 0 < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)
⊢ (p : (a : E) → ℝ) x < HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
exact lt_mul_of_one_lt_left hpx one_lt_two

Premises used: one_lt_two, lt_mul_of_one_lt_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x

Tactic:
IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp

Premises used: gauge, le_of_forall_pos_le_add, IsGLB.csInf_eq, And.intro
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
h : ∀ (r : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1} r → (p : (a : E) → ℝ) x ≤ r
h₁ :
  ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r) (ε : ℝ)
    (hε : 0 < ε), r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ gauge (p.ball 0 1) x = (p : (a : E) → ℝ) x

Tactic:
refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp

Premises used: IsGLB.csInf_eq, And.intro
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ p.ball 0 1
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
⊢ LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)

Tactic:
rw [p.mem_ball_zero] at hy

Premises used: Seminorm.mem_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ p.ball 0 1
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
hy₁ : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
⊢ Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}

Tactic:
rw [p.mem_ball_zero] at hy

Premises used: Seminorm.mem_ball_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
h : HMul.hMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ) ≤ r
⊢ (p : (a : E) → ℝ) ((fun (x : E) ↦ r • x) y) ≤ r

Tactic:
rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos hr]

Premises used: SeminormClass.map_smul_eq_mul, abs_of_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
⊢ HMul.hMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ) ≤ r

Tactic:
mul_le_of_le_one_right hr.le hy.le

Premises used: mul_le_of_le_one_right, LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : LT.lt (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) (1 : ℝ)
hp : Set.Nonempty (α := ℝ) {r_1 : ℝ | 0 < r_1 ∧ (fun (x : E) ↦ r • x) y ∈ r_1 • p.ball 0 1}
⊢ HMul.hMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ) ≤ r

Tactic:
exact mul_le_of_le_one_right hr.le hy.le

Premises used: mul_le_of_le_one_right, LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
⊢ 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
⊢ 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
have hpε : 0 < p x + ε := by positivity
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩

Premises used: smul_inv_smul₀, LT.lt.ne', Inv.inv, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
h : (HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε)⁻¹ • x ∈ p.ball 0 1
⊢ r ≤ HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩

Premises used: smul_inv_smul₀, LT.lt.ne', Inv.inv, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
h : (p : (a : E) → ℝ) x < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ (HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε)⁻¹ • x ∈ p.ball 0 1

Tactic:
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε),
      inv_mul_lt_iff₀ hpε, mul_one]

Premises used: Iff.mpr, Seminorm.mem_ball_zero, inv_mul_lt_iff₀, inv_pos, SeminormClass.map_smul_eq_mul, abs_of_pos, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ (p : (a : E) → ℝ) x < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
x : E
hp : Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}
r : ℝ
hr : Membership.mem (γ := Set ℝ) (lowerBounds {r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1}) r
ε : ℝ
hε : 0 < ε
hpε : 0 < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ (p : (a : E) → ℝ) x < HAdd.hAdd (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
exact lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
p : Seminorm ℝ E
⊢ gaugeSeminorm (s := p.ball 0 1) ⋯ ⋯ ⋯ = p

Tactic:
DFunLike.coe_injective p.gauge_ball

Premises used: DFunLike.coe_injective, Seminorm.gauge_ball
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
rw : gauge (Seminorm.ball (normSeminorm ℝ E) 0 1) x = ‖x‖
rw₁ : (normSeminorm ℝ E : (a : E) → ℝ) x = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ gauge (ball 0 1) x = ‖x‖

Tactic:
rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]

Premises used: Real, ball_normSeminorm, coe_normSeminorm, Seminorm.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
inl : ∀ (hr : LE.le (α := ℝ) 0 0), gauge (ball 0 0) x = ‖x‖ / 0
inr : ∀ (hr : 0 < r), gauge (ball 0 r) x = ‖x‖ / r
⊢ gauge (ball 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
⊢ gauge (ball 0 0) x = ‖x‖ / 0

Tactic:
simp