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
hs : Balanced ℝ s
x : E
hx : x ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
rwa rwa₁ rwa₂ rwa₃ : a ≤ 1
⊢ ‖a‖ ≤ 1

Tactic:
rwa [Real.norm_of_nonneg ha₀]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Tactic:
rw [starConvex_zero_iff] at hs₀

Premises used: starConvex_zero_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
hs₁ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
⊢ Absorbs ℝ s {x}

Tactic:
rw [starConvex_zero_iff] at hs₀

Premises used: starConvex_zero_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
hs₁ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₃ : Absorbs ℝ s {x}
⊢ x ∉ a • s

Tactic:
rw [starConvex_zero_iff] at hs₀

Premises used: starConvex_zero_iff
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
obtain : ∀ (r : ℝ) (hr : r > 0) (h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s), a ≤ gauge s x
⊢ a ≤ gauge s x

Tactic:
obtain ⟨r, hr, h⟩ := hs₂.exists_pos

Premises used: Absorbs.exists_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
r : ℝ
hr : r > 0
h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s
⊢ a ≤ gauge s x

Tactic:
le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_

Premises used: Set.singleton_subset_iff, Eq.ge, gauge, le_csInf, LT.lt.le, And.intro, Exists.intro, Iff.mp, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
r : ℝ
hr : r > 0
h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s
refine : ∀ (b : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | 0 < r ∧ x ∈ r • s} b → a ≤ b
⊢ a ≤ gauge s x

Tactic:
refine le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
⊢ a ≤ b

Tactic:
not_lt.1 fun hba => hx ?_

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
refine : ∀ (hba : b < a), (fun (x : E) ↦ b • x) x ∈ a • s
⊢ a ≤ b

Tactic:
refine not_lt.1 fun hba => hx ?_

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
⊢ 0 < a

Tactic:
have ha := hb.trans hba
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ 0 ≤ a⁻¹ * b

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
refine_1 : a⁻¹ * b ≤ 1
refine_2 : Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ a • x) ((a⁻¹ * b) • x)) ((fun (x : E) ↦ b • x) x)
⊢ (fun (x : E) ↦ b • x) x ∈ a • s

Tactic:
refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
refine_1 : b / a ≤ 1
⊢ a⁻¹ * b ≤ 1

Tactic:
rw [← div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1

Tactic:
div_le_one_of_le₀ hba.le ha.le

Premises used: div_le_one_of_le₀, LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ b / a ≤ 1

Tactic:
exact div_le_one_of_le₀ hba.le ha.le

Premises used: div_le_one_of_le₀, LT.lt.le
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun (x : E) ↦ b • x) x}
hx : (fun (x : E) ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun (x : E) ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
refine_2 : (a * (a⁻¹ * b)) • x = b • x
refine_2₁ refine_2₂ : b • x = b • x
⊢ a • (a⁻¹ * b) • x = b • x

Tactic:
rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']

Premises used: mul_inv_cancel_left₀, LT.lt.ne', SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
hs₁ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx rwa rwa₁ rwa₂ rwa₃ : x ∉ s
⊢ x ∉ HSMul.hSMul (α := ℝ) 1 s

Tactic:
rwa [one_smul]

Premises used: one_smul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
inl :
  ∀ (ha : LE.le.{u_3} (α := α) 0 0),
    gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
inr : ∀ (ha' : 0 < a), gauge s (a • x) = a • gauge s x
⊢ gauge s (a • x) = a • gauge s x

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
x : E
ha : LE.le.{u_3} (α := α) 0 0
inl : gauge s 0 = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
inl₁ : 0 = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)

Tactic:
rw [zero_smul, gauge_zero, zero_smul]

Premises used: zero_smul, gauge_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
inr :
  sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} =
    sInf (HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
⊢ gauge s (a • x) = a • gauge s x

Tactic:
rw [gauge_def', gauge_def', ← Real.sInf_smul_of_nonneg ha]

Premises used: gauge_def', Real.sInf_smul_of_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
inr :
  {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} =
    HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
⊢ sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} =
    sInf (HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
inr :
  ∀ (r : ℝ),
    Membership.mem (γ := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} r ↔
      r ∈ HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
⊢ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} =
    HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}

Tactic:
ext r
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
inr :
  Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s →
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
inr₁ :
  (∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r) →
    Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • a • x ∈ s
⊢ 0 < r

Tactic:
simp_rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : r⁻¹ • a • x ∈ s
hr : 0 < r
⊢ a • x ∈ r • s

Tactic:
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx

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
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : r⁻¹ • a • x ∈ s
hr : 0 < r
hx₁ : a • x ∈ r • s
⊢ 0 < r

Tactic:
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx

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
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
⊢ 0 < a⁻¹ • r

Tactic:
have := smul_pos (inv_pos.2 ha') hr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩

Premises used: smul_inv_smul₀, LT.lt.ne', Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
inr : (a⁻¹ • r)⁻¹ • x ∈ s
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r

Tactic:
refine ⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hx : a • x ∈ r • s
hr : 0 < r
this : 0 < a⁻¹ • r
inr : x ∈ (a⁻¹ • r) • s
inr₁ : x ∈ a⁻¹ • r • s
inr₂ : a⁻¹⁻¹ • x ∈ r • s
inr₃ inr₄ inr₅ inr₆ : a • x ∈ r • s
⊢ (a⁻¹ • r)⁻¹ • x ∈ s

Tactic:
rwa [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc,
      mem_smul_set_iff_inv_smul_mem₀ (inv_ne_zero ha'.ne'), inv_inv]

Premises used: smul_assoc, LT.lt.ne', inv_inv, inv_ne_zero, 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
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • x ∈ s
⊢ 0 < r

Tactic:
rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • x ∈ s
hr₁ : 0 < r
⊢ r⁻¹ • x ∈ s

Tactic:
rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ x ∈ r • s

Tactic:
rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx

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
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
⊢ 0 < a • r

Tactic:
have := smul_pos ha' hr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
⟨this, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
inr : (a • r)⁻¹ • a • x ∈ s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
refine ⟨this, ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
inr : a • x ∈ a • r • s
⊢ (a • r)⁻¹ • a • x ∈ s

Tactic:
rw [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc]

Premises used: smul_assoc, 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
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s

Tactic:
smul_mem_smul_set hx

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : IsScalarTower.{u_3, 0, u_2} α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ a • x ∈ a • r • s

Tactic:
exact smul_mem_smul_set hx

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
inl :
  ∀ (ha : LE.le.{u_3} (α := α) 0 0),
    gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0⁻¹ (gauge s)
inr : ∀ (ha' : 0 < a), gauge (a • s) = a⁻¹ • gauge s
⊢ gauge (a • s) = a⁻¹ • gauge s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
ha : LE.le.{u_3} (α := α) 0 0
inl : gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 (gauge s)
inl₁ : gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = 0
inl₂ inl₃ : Eq.{u_2 + 1} (α := (x : E) → ℝ) 0 0
⊢ gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0⁻¹ (gauge s)

Tactic:
rw [inv_zero, zero_smul, gauge_of_subset_zero (zero_smul_set_subset _)]

Premises used: inv_zero, gauge_of_subset_zero, zero_smul, Set.zero_smul_set_subset
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
inr : ∀ (x : E), gauge (a • s) x = (a⁻¹ • gauge s) x
⊢ gauge (a • s) = a⁻¹ • gauge s

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
inr :
  sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
    sInf (HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
⊢ gauge (a • s) x = (a⁻¹ • gauge s) x

Tactic:
rw [gauge_def', Pi.smul_apply, gauge_def', ← Real.sInf_smul_of_nonneg (inv_nonneg.2 ha)]

Premises used: Iff.mpr, gauge_def', Real.sInf_smul_of_nonneg, inv_nonneg, Pi.smul_apply