awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)
have obtain : ∀ (y' : α) (hy'' : y = (f : (a : α) → β) y'),
  HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)
Tactic: obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)
have simp : a • x' + b • y' ≤
  (f.symm : (a : β) → α)
    (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
Tactic: simp only [hx'', hy'', OrderIso.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ a • x' + b • y' ≤
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
have rw : (f : (a : α) → β) (a • x' + b • y') ≤
  HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)
Tactic: rw [← f.le_iff_le, OrderIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
⊢ x = y
have by_contra : ∀ (hxy : ¬x = y), False
Tactic: by_contra hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
⊢ False
have hz : z ∈ s
Tactic: have hz : z ∈ s := hf.1 hx hy (by simp) (by simp) <| by norm_num
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ False
have refine : f z < f z
Tactic: refine lt_irrefl (f z) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z)
have h₁ : f x ≤ f z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
h₁ : f x ≤ f z
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z)
have h₂ : f y ≤ f z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) = f z
have rw : HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • f z = f z
Tactic: rw [← _root_.add_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ f z < f z
have f₁ : HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f y) ≤
  HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z)
Tactic: calc
    f z < _ := hf.2 hx hy hxy (by simp) (by simp) <| by norm_num
    _ ≤ (2 : 𝕜)⁻¹ • f z + (2 : 𝕜)⁻¹ • f z := by gcongr; exacts [hfx hz, hfy hz]
    _ = f z := by rw [← _root_.add_smul]; norm_num
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
f₁ :
  HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z)
⊢ f z < f z
have f₂ : HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) = f z
Tactic: calc
    f z < _ := hf.2 hx hy hxy (by simp) (by simp) <| by norm_num
    _ ≤ (2 : 𝕜)⁻¹ • f z + (2 : 𝕜)⁻¹ • f z := by gcongr; exacts [hfx hz, hfy hz]
    _ = f z := by rw [← _root_.add_smul]; norm_num
-- Lean 4 proof step from Mathlib.Analysis.Convex.FunctionTopology (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : PartialOrder β
inst_3 : TopologicalSpace β
inst_4 : OrderClosedTopology β
inst_5 : AddCommMonoid α
inst_6 : AddCommMonoid β
inst_7 : SMul 𝕜 α
inst_8 : SMul 𝕜 β
inst_9 : ContinuousConstSMul 𝕜 β
inst_10 : ContinuousAdd β
s : Set α
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | ConvexOn 𝕜 s f}
have simp : IsClosed[Pi.topologicalSpace]
  ({a : α → β | Convex 𝕜 s} ∩
    ⋂ i ∈ s,
      ⋂ i_1 ∈ s,
        ⋂ (i_2 : 𝕜),
          ⋂ (i_3 : 𝕜),
            ⋂ (_ : 0 ≤ i_2),
              ⋂ (_ : 0 ≤ i_3), ⋂ (_ : i_2 + i_3 = 1), {x : α → β | x (i_2 • i + i_3 • i_1) ≤ i_2 • x i + i_3 • x i_1})
Tactic: simp only [ConvexOn, setOf_and, setOf_forall]
-- Lean 4 proof step from Mathlib.Analysis.Convex.FunctionTopology (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : PartialOrder β
inst_3 : TopologicalSpace β
inst_4 : OrderClosedTopology β
inst_5 : AddCommMonoid α
inst_6 : AddCommMonoid β
inst_7 : SMul 𝕜 α
inst_8 : SMul 𝕜 β
inst_9 : ContinuousConstSMul 𝕜 β
inst_10 : ContinuousAdd β
s : Set α
⊢ IsClosed[Pi.topologicalSpace]
    ({a : α → β | Convex 𝕜 s} ∩
      ⋂ i ∈ s,
        ⋂ i_1 ∈ s,
          ⋂ (i_2 : 𝕜),
            ⋂ (i_3 : 𝕜),
              ⋂ (_ : 0 ≤ i_2),
                ⋂ (_ : 0 ≤ i_3), ⋂ (_ : i_2 + i_3 = 1), {x : α → β | x (i_2 • i + i_3 • i_1) ≤ i_2 • x i + i_3 • x i_1})
have refine : IsClosed[Pi.topologicalSpace]
  (⋂ i ∈ s,
    ⋂ i_1 ∈ s,
      ⋂ (i_2 : 𝕜),
        ⋂ (i_3 : 𝕜),
          ⋂ (_ : 0 ≤ i_2),
            ⋂ (_ : 0 ≤ i_3), ⋂ (_ : i_2 + i_3 = 1), {x : α → β | x (i_2 • i + i_3 • i_1) ≤ i_2 • x i + i_3 • x i_1})
Tactic: refine IsClosed.inter isClosed_const ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
⊢ gauge s x = sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
have congrm : ∀ (r : ℝ), 0 < r ∧ x ∈ r • s ↔ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s
Tactic: congrm sInf {r | ?_}
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x : E
⊢ LE.le (α := (fun (x : E) ↦ ℝ) x) (sInf {r : ℝ | 0 < r ∧ x ∈ r • t}) (sInf {r : ℝ | 0 < r ∧ x ∈ r • s})
have ht : BddBelow (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • t}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x : E
ht : BddBelow (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • t}
⊢ LE.le (α := (fun (x : E) ↦ ℝ) x) (sInf {r : ℝ | 0 < r ∧ x ∈ r • t}) (sInf {r : ℝ | 0 < r ∧ x ∈ r • s})
have hs₁ : Set.Nonempty (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • s}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
absorbs : Absorbent ℝ s
h : gauge s x < a
⊢ ∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s
have obtain : ∀ (b : ℝ) (hba : b < a) (hb : 0 < b) (hx : x ∈ b • s), ∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s
Tactic: obtain ⟨b, ⟨hb, hx⟩, hba⟩ := exists_lt_of_csInf_lt absorbs.gauge_set_nonempty h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ gauge s 0 = 0
have rw : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
Tactic: rw [gauge_def']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
have pos : ∀ (h : 0 ∈ s), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
Tactic: by_cases h : (0 : E) ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
pos :
  ∀ (h : 0 ∈ s), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
have neg : ∀ (h : 0 ∉ s), Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
Tactic: by_cases h : (0 : E) ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge 0) 0
have h : ∀ (x : E), gauge 0 x = 0 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
x : E
⊢ gauge 0 x = 0 x
have h : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
Tactic: rw [gauge_def']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
have h : Eq (α := ℝ)
  (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (HSMul.hSMul (β := E) r⁻¹ 0)})
  (0 0)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
h :
  Eq (α := ℝ)
    (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (HSMul.hSMul (β := E) r⁻¹ 0)})
    (0 0)
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
have h₁ : ∀ (hx : x ≠ 0),
  Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
have h : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)}) 0
Tactic: simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)}) 0
have h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)} ∅
Tactic: convert! Real.sInf_empty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0
have h : ∀ (x : E), gauge ∅ x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
h : s ⊆ 0
⊢ gauge s = 0
have inl : ∀ (h : Subset.{u_2} (α := Set E) ∅ 0), Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0
Tactic: obtain rfl | rfl := subset_singleton_iff_eq.1 h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
h : s ⊆ 0
inl : ∀ (h : Subset.{u_2} (α := Set E) ∅ 0), Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0
⊢ gauge s = 0
have inr : ∀ (h : Subset (α := Set E) {0} 0), Eq (α := (x : E) → ℝ) (gauge {0}) 0
Tactic: obtain rfl | rfl := subset_singleton_iff_eq.1 h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
⊢ gauge s (-x) = gauge s x
have this : ∀ (x : E), -x ∈ s ↔ x ∈ s
Tactic: have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
⊢ gauge s (-x) = gauge s x
have simp_rw : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • -x ∈ s})
  (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
Tactic: simp_rw [gauge_def', smul_neg, this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
simp_rw :
  Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • -x ∈ s})
    (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
⊢ gauge s (-x) = gauge s x
have simp_rw₁ : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ -(r⁻¹ • x) ∈ s})
  (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
Tactic: simp_rw [gauge_def', smul_neg, this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
⊢ gauge (-s) (-x) = gauge s x
have simp_rw : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • -x ∈ -s})
  (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
Tactic: simp_rw [gauge_def', smul_neg, neg_mem_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
simp_rw :
  Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • -x ∈ -s})
    (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
⊢ gauge (-s) (-x) = gauge s x
have simp_rw₁ : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ -(r⁻¹ • x) ∈ -s})
  (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})
Tactic: simp_rw [gauge_def', smul_neg, neg_mem_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
⊢ gauge (-s) x = gauge s (-x)
have rw : gauge (- -s) (-x) = gauge s (-x)
Tactic: rw [← gauge_neg_set_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
rw : gauge (- -s) (-x) = gauge s (-x)
⊢ gauge (-s) x = gauge s (-x)
have rw₁ : gauge s (-x) = gauge s (-x)
Tactic: rw [← gauge_neg_set_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
⊢ gauge s x ≤ a
have inl : ∀ (ha : LE.le (α := ℝ) 0 0) (hx : x ∈ HSMul.hSMul (α := ℝ) 0 s), gauge s x ≤ 0
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
inl : ∀ (ha : LE.le (α := ℝ) 0 0) (hx : x ∈ HSMul.hSMul (α := ℝ) 0 s), gauge s x ≤ 0
⊢ gauge s x ≤ a
have inr : ∀ (ha' : 0 < a), gauge s x ≤ a
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
s : Set E
x : E
ha : LE.le (α := ℝ) 0 0
hx : x ∈ HSMul.hSMul (α := ℝ) 0 s
⊢ gauge s x ≤ 0
have inl : gauge s 0 ≤ 0
Tactic: rw [mem_singleton_iff.1 (zero_smul_set_subset _ hx), gauge_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
⊢ Eq.{u_2 + 1} (α := Set E) {x : E | gauge s x ≤ a} (⋂ (r : ℝ), ⋂ (_ : a < r), r • s)
have h : ∀ (x : E),
  Membership.mem (γ := Set E) {x : E | gauge s x ≤ a} x ↔
    Membership.mem (γ := Set E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • 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
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ Membership.mem (γ := Set E) {x : E | gauge s x ≤ a} x ↔
    Membership.mem (γ := Set E) (⋂ (r : ℝ), ⋂ (_ : a < r), r • s) x
have h : gauge s x ≤ a ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
Tactic: simp_rw [Set.mem_iInter, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
have h : ∀ (h : gauge s x ≤ a) (r : ℝ) (hr : a < r), x ∈ r • s
Tactic: refine ⟨fun h r hr => ?_, fun h => le_of_forall_pos_lt_add fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : ∀ (h : gauge s x ≤ a) (r : ℝ) (hr : a < r), x ∈ r • s
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s
have h₁ : ∀ (h : ∀ (i : ℝ) (i_1 : a < i), x ∈ i • s) (ε : ℝ) (hε : 0 < ε), gauge s x < a + ε
Tactic: refine ⟨fun h r hr => ?_, fun h => le_of_forall_pos_lt_add fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
⊢ x ∈ r • s
have hr' : 0 < r
Tactic: have hr' := ha.trans_lt hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
⊢ x ∈ r • s
have h₁ : r⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ hr'.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
⊢ r⁻¹ • x ∈ s
have h₁ : ∀ (δ : ℝ) (δ_pos : 0 < δ) (hδr : δ < r) (hδ : x ∈ δ • s), r⁻¹ • x ∈ s
Tactic: obtain ⟨δ, δ_pos, hδr, hδ⟩ := exists_lt_of_gauge_lt hs₂ (h.trans_lt hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
this : (r⁻¹ * δ) • δ⁻¹ • x ∈ s
⊢ r⁻¹ • x ∈ s
have rwa : ∀ (this : (r⁻¹ * δ * δ⁻¹) • x ∈ s), r⁻¹ • x ∈ s
Tactic: rwa [smul_smul, mul_inv_cancel_right₀ δ_pos.ne'] at this
Cleared hypotheses: this