awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Function
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 x ≤ f z

Tactic:
exacts [hfx hz, hfy hz]
-- Module: Mathlib.Analysis.Convex.Function
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
rw : HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • f z = f z
⊢ 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:
rw [← _root_.add_smul]

Premises used: add_smul
-- Module: Mathlib.Analysis.Convex.Function
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
⊢ HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • f z = f z

Tactic:
norm_num
-- Module: Mathlib.Analysis.Convex.Function
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₂ : 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 < 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

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Function
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 : StrictConcaveOn 𝕜 s f
hfx : IsMaxOn f s x
hfy : IsMaxOn f s y
hx : x ∈ s
hy : y ∈ s
⊢ x = y

Tactic:
hf.dual.eq_of_isMinOn hfx hfy hx hy

Premises used: StrictConvexOn.eq_of_isMinOn, StrictConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : PosSMulStrictMono 𝕜 β
x y z : 𝕜
s : Set 𝕜
f : 𝕜 → β
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y ≤ z
h : f x ≤ f y
⊢ f y ≤ f z

Tactic:
hyz.eq_or_lt.elim (fun hyz => (congr_arg f hyz).le) fun hyz =>
    hf.le_right_of_left_le hx hz (Ioo_subset_openSegment ⟨hxy, hyz⟩) h

Premises used: ConvexOn.le_right_of_left_le, LE.le.eq_or_lt, Eq.le, congr_arg, Ioo_subset_openSegment, And.intro, Or.elim
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : PosSMulStrictMono 𝕜 β
x y z : 𝕜
s : Set 𝕜
f : 𝕜 → β
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hz : z ∈ s
hxy : x ≤ y
hyz : y < z
h : f z ≤ f y
⊢ f y ≤ f x

Tactic:
hxy.eq_or_lt.elim (fun hxy => (congr_arg f hxy).ge) fun hxy =>
    hf.le_left_of_right_le hx hz (Ioo_subset_openSegment ⟨hxy, hyz⟩) h

Premises used: LE.le.eq_or_lt, Eq.ge, congr_arg, Ioo_subset_openSegment, And.intro, ConvexOn.le_left_of_right_le, Or.elim
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : PosSMulStrictMono 𝕜 β
x y z : 𝕜
s : Set 𝕜
f : 𝕜 → β
hf : ConcaveOn 𝕜 s f
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y ≤ z
h : f y ≤ f x
⊢ f z ≤ f y

Tactic:
hf.dual.le_right_of_left_le'' hx hz hxy hyz h

Premises used: ConvexOn.le_right_of_left_le'', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : PosSMulStrictMono 𝕜 β
x y z : 𝕜
s : Set 𝕜
f : 𝕜 → β
hf : ConcaveOn 𝕜 s f
hx : x ∈ s
hz : z ∈ s
hxy : x ≤ y
hyz : y < z
h : f y ≤ f z
⊢ f x ≤ f y

Tactic:
hf.dual.le_left_of_right_le'' hx hz hxy hyz h

Premises used: ConvexOn.le_left_of_right_le'', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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 α
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})
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | ConvexOn 𝕜 s f}

Tactic:
simp only [ConvexOn, setOf_and, setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall, ConvexOn
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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})

Tactic:
IsClosed.inter isClosed_const ?_

Premises used: isClosed_const, IsClosed.inter
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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 α
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})
⊢ 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:
refine IsClosed.inter isClosed_const ?_

Premises used: isClosed_const, IsClosed.inter
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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 α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (x_1 : α → β) ↦ x_1 (a • x + b • y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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 α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Continuous[Pi.topologicalSpace, inst_3] fun (x_1 : α → β) ↦ a • x_1 x + b • x_1 y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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]
    (⋂ 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:
exact isClosed_iInter fun x => isClosed_iInter fun hx => isClosed_iInter fun y =>
      isClosed_iInter fun hy => isClosed_iInter fun a => isClosed_iInter fun b =>
      isClosed_iInter fun ha => isClosed_iInter fun hb => isClosed_iInter fun hab =>
      isClosed_le (by fun_prop) (by fun_prop)

Premises used: isClosed_le, isClosed_iInter
-- Module: Mathlib.Analysis.Convex.FunctionTopology
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 : α → β | ConcaveOn 𝕜 s f}

Tactic:
isClosed_setOf_convexOn (α := α) (β := βᵒᵈ)

Premises used: setOf, OrderDual, ConcaveOn, isClosed_setOf_convexOn
-- Module: Mathlib.Analysis.Convex.Gauge
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 ∧ x ∈ r • s}

Tactic:
rfl

Premises used: Set.Ioi, gauge, Set.Mem, setOf, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
congrm : ∀ (r : ℝ), 0 < r ∧ x ∈ r • s ↔ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s
⊢ gauge s x = sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}

Tactic:
congrm sInf {r | ?_}

Premises used: setOf, InfSet.sInf
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
r : ℝ
⊢ 0 < r ∧ x ∈ r • s ↔ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s

Tactic:
and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _

Premises used: Set.Ioi, Set.Mem, setOf, and_congr_right, LT.lt.ne', Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
r : ℝ
⊢ 0 < r ∧ x ∈ r • s ↔ Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s

Tactic:
exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _

Premises used: and_congr_right, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
⊢ BddBelow (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • s}

Tactic:
⟨0, fun _ hr => hr.1.le⟩

Premises used: LT.lt.le, Set.Nonempty, And.left, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
absorbs : Absorbent ℝ s
⊢ Set.Nonempty (α := ℝ) {r : ℝ | 0 < r ∧ x ∈ r • s}

Tactic:
let ⟨r, hr₁, hr₂⟩ := (absorbs x).exists_pos
  ⟨r, hr₁, hr₂ r (Real.norm_of_nonneg hr₁.le).ge rfl⟩

Premises used: Eq.ge, setOf, Membership.mem, LT.lt.le, And, Set.Nonempty, And.intro, LT.lt, Absorbs.exists_pos, Exists.intro, HSMul.hSMul, OfNat.ofNat, _private.0.Absorbent.gauge_set_nonempty.match_1, rfl, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
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}
hs₁ : Set.Nonempty (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • s}
⊢ LE.le (α := (fun (x : E) ↦ ℝ) x) (sInf {r : ℝ | 0 < r ∧ x ∈ r • t}) (sInf {r : ℝ | 0 < r ∧ x ∈ r • s})

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x : E
⊢ BddBelow (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • t}

Tactic:
gauge_set_bddBelow

Premises used: _private.0.gauge_set_bddBelow
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x : E
⊢ Set.Nonempty (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • s}

Tactic:
hs.gauge_set_nonempty

Premises used: Absorbent.gauge_set_nonempty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s t : Set E
hs : Absorbent ℝ s
h : s ⊆ t
x : E
⊢ BddBelow (α := (fun (x : E) ↦ ℝ) x) {r : ℝ | 0 < r ∧ x ∈ r • t}

Tactic:
exacts [gauge_set_bddBelow, hs.gauge_set_nonempty]

Premises used: Absorbent.gauge_set_nonempty, _private.0.gauge_set_bddBelow
-- Module: Mathlib.Analysis.Convex.Gauge
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
obtain : ∀ (b : ℝ) (hba : b < a) (hb : 0 < b) (hx : x ∈ b • s), ∃ (b : ℝ), 0 < b ∧ b < a ∧ 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

Premises used: Absorbent.gauge_set_nonempty, exists_lt_of_csInf_lt
-- Module: Mathlib.Analysis.Convex.Gauge
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 : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s

Tactic:
⟨b, hb, hba, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Gauge
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 : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s

Tactic:
exact ⟨b, hb, hba, hx⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
rw : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0
⊢ gauge s 0 = 0

Tactic:
rw [gauge_def']

Premises used: gauge_def'
-- Module: Mathlib.Analysis.Convex.Gauge
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
neg :
  ∀ (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

Tactic:
by_cases h : (0 : E) ∈ s

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
h : 0 ∈ s
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0

Tactic:
simp only [smul_zero, sep_true, h, csInf_Ioi]

Premises used: Set.sep_true, smul_zero, csInf_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ HSMul.hSMul (β := E) r⁻¹ 0 ∈ s}) 0

Tactic:
simp only [smul_zero, sep_false, h, Real.sInf_empty]

Premises used: smul_zero, Set.sep_false, Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
h : ∀ (x : E), gauge 0 x = 0 x
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge 0) 0

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Gauge
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 (r⁻¹ • x)}) (0 x)
⊢ gauge 0 x = 0 x

Tactic:
rw [gauge_def']

Premises used: gauge_def'
-- Module: Mathlib.Analysis.Convex.Gauge
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)
h₁ :
  ∀ (hx : x ≠ 0),
    Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
⊢ Eq (α := ℝ)
    (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (HSMul.hSMul (β := E) r⁻¹ 0)})
    (0 0)

Tactic:
simp only [csInf_Ioi, mem_zero, Pi.zero_apply, sep_true, smul_zero]

Premises used: Set.sep_true, smul_zero, Pi.zero_apply, csInf_Ioi, Set.mem_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
h : Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)}) 0
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ Membership.mem (γ := Set E) 0 (r⁻¹ • x)}) (0 x)

Tactic:
simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]

Premises used: inv_eq_zero, Pi.zero_apply, Set.mem_zero, smul_eq_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
⊢ Eq (α := ℝ) (sInf ∅) 0

Tactic:
Real.sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
h : Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)} ∅
⊢ Eq (α := ℝ) (sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)}) 0

Tactic:
convert! Real.sInf_empty

Premises used: Real.sInf_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)} ∅

Tactic:
eq_empty_iff_forall_notMem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx

Premises used: Iff.mpr, ne_of_gt, And.right, And.left, Set.eq_empty_iff_forall_notMem, Or.elim
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
hx : x ≠ 0
⊢ Eq (α := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ (r = 0 ∨ x = 0)} ∅

Tactic:
exact eq_empty_iff_forall_notMem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx

Premises used: Iff.mpr, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
h : ∀ (x : E), gauge ∅ x = 0 x
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
x : E
⊢ gauge ∅ x = 0 x

Tactic:
simp only [gauge_def', Real.sInf_empty, mem_empty_iff_false, Pi.zero_apply, sep_false]

Premises used: gauge_def', Pi.zero_apply, Set.sep_false, Real.sInf_empty, Set.mem_empty_iff_false
-- Module: Mathlib.Analysis.Convex.Gauge
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
inr : ∀ (h : Subset (α := Set E) {0} 0), Eq (α := (x : E) → ℝ) (gauge {0}) 0
⊢ gauge s = 0

Tactic:
obtain rfl | rfl := subset_singleton_iff_eq.1 h

Premises used: Iff.mp, Set.subset_singleton_iff_eq, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
h : Subset.{u_2} (α := Set E) ∅ 0
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0

Tactic:
gauge_empty

Premises used: gauge_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
h : Subset (α := Set E) {0} 0
⊢ Eq (α := (x : E) → ℝ) (gauge {0}) 0

Tactic:
gauge_zero'

Premises used: gauge_zero'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
h : Subset.{u_2} (α := Set E) ∅ 0
⊢ Eq.{u_2 + 1} (α := (x : E) → ℝ) (gauge ∅) 0

Tactic:
exacts [gauge_empty, gauge_zero']

Premises used: gauge_zero', gauge_empty
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
⊢ 0 ≤ gauge s x

Tactic:
Real.sInf_nonneg fun _ hx => hx.1.le

Premises used: gauge, LT.lt.le, Real.sInf_nonneg, And.left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x_1 x : E
h : -x ∈ s
⊢ x ∈ s

Tactic:
simpa using symmetric _ h
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
⊢ ∀ (x : E), -x ∈ s ↔ x ∈ s

Tactic:
have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩
-- Module: Mathlib.Analysis.Convex.Gauge
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})
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

Tactic:
simp_rw [gauge_def', smul_neg, this]

Premises used: gauge_def', smul_neg
-- Module: Mathlib.Analysis.Convex.Gauge
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})
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

Tactic:
simp_rw [gauge_def', smul_neg, neg_mem_neg]

Premises used: gauge_def', smul_neg, Set.neg_mem_neg