awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
have inl : gauge s 0 = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
Tactic: rw [zero_smul, gauge_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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)
⊢ gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
have inl₁ : 0 = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
Tactic: rw [zero_smul, gauge_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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)
⊢ gauge s (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 x) = HSMul.hSMul.{u_3, 0, 0} (α := α) 0 (gauge s x)
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [zero_smul, gauge_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge s (a • x) = a • gauge s x
have 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})
Tactic: rw [gauge_def', gauge_def', ← Real.sInf_smul_of_nonneg ha]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ 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})
have 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}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s} =
    HSMul.hSMul (β := Set ℝ) a {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
have 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}
Tactic: ext r
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have inr : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have inr₁ : (∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r) →
  Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • a • x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
⊢ ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have hr₁ : 0 < r
Tactic: simp_rw [mem_Ioi] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have hx₁ : a • x ∈ r • s
Tactic: rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
Cleared hypotheses: hx, hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a • y = r
have this : 0 < a⁻¹ • r
Tactic: have := smul_pos (inv_pos.2 ha') hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
have inr : (a⁻¹ • r)⁻¹ • x ∈ s
Tactic: refine ⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
have inr : x ∈ (a⁻¹ • r) • 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
have inr₁ : x ∈ a⁻¹ • r • 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ (a⁻¹ • r)⁻¹ • x ∈ s
have inr₂ : a⁻¹⁻¹ • x ∈ r • 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (a • r) ∧ (a • r)⁻¹ • a • x ∈ s
have hr₁ : 0 < r
Tactic: rw [mem_Ioi] at hr ⊢
Cleared hypotheses: hr, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
have hx₁ : x ∈ r • s
Tactic: rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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 ∧ (a • r)⁻¹ • a • x ∈ s
have this : 0 < a • r
Tactic: have := smul_pos ha' hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
have inr : (a • r)⁻¹ • a • x ∈ s
Tactic: refine ⟨this, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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 • r)⁻¹ • a • x ∈ s
have inr : a • x ∈ a • r • s
Tactic: rw [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (a • s) = a⁻¹ • gauge s
have 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)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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)
⊢ gauge (a • s) = a⁻¹ • gauge s
have inr : ∀ (ha' : 0 < a), gauge (a • s) = a⁻¹ • gauge s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0⁻¹ (gauge s)
have inl : 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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)
⊢ gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0⁻¹ (gauge s)
have inl₁ : gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = 0
Tactic: rw [inv_zero, zero_smul, gauge_of_subset_zero (zero_smul_set_subset _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0 s) = HSMul.hSMul.{u_3, u_2, u_2} (α := α) 0⁻¹ (gauge s)
have inl₂ : Eq.{u_2 + 1} (α := (x : E) → ℝ) 0 0
Tactic: rw [inv_zero, zero_smul, gauge_of_subset_zero (zero_smul_set_subset _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (a • s) = a⁻¹ • gauge s
have inr : ∀ (x : E), gauge (a • s) x = (a⁻¹ • gauge s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ gauge (a • s) x = (a⁻¹ • gauge s) x
have 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})
Tactic: rw [gauge_def', Pi.smul_apply, gauge_def', ← Real.sInf_smul_of_nonneg (inv_nonneg.2 ha)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ 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})
have inr : {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
  HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
⊢ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
    HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
have inr : ∀ (r : ℝ),
  Membership.mem (γ := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} r ↔
    r ∈ HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
Tactic: ext r
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
r : ℝ
⊢ (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
have inr : (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) →
  ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
r : ℝ
inr :
  (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) →
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
⊢ (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
have inr₁ : (∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r) →
  Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
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
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
⊢ ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
have hr₁ : 0 < r
Tactic: simp_rw [mem_Ioi] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
have inr : (a • r)⁻¹ • x ∈ s
Tactic: refine ⟨a • r, ⟨smul_pos ha' hr, ?_⟩, inv_smul_smul₀ ha'.ne' _⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
⊢ (a • r)⁻¹ • x ∈ s
have inr : (a⁻¹ • r⁻¹) • x ∈ s
Tactic: rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
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
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
inr : (a⁻¹ • r⁻¹) • x ∈ s
⊢ (a • r)⁻¹ • x ∈ s
have inr₁ : a⁻¹ • r⁻¹ • x ∈ s
Tactic: rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']