awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (E := E) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Premises used: Convex.prod, Convex.is_linear_image, IsLinearMap.isLinearMap_add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
⊢ (↑(convexAddSubmonoid 𝕜 E) : Set (Set E)) = {s : Set E | Convex 𝕜 s}

Tactic:
rfl

Premises used: setOf, Convex, rfl
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Membership.mem (γ := AddSubmonoid (Set E)) (convexAddSubmonoid 𝕜 E) s ↔ Convex 𝕜 s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
l : List (Set E)
h : ∀ i ∈ l, Convex 𝕜 i
⊢ Convex 𝕜 l.sum

Tactic:
(convexAddSubmonoid 𝕜 E).list_sum_mem h

Premises used: Set.Mem, convexAddSubmonoid, AddSubmonoid.list_sum_mem, setOf, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Multiset (Set E)
h : ∀ i ∈ s, Convex 𝕜 i
⊢ Convex 𝕜 s.sum

Tactic:
(convexAddSubmonoid 𝕜 E).multiset_sum_mem _ h

Premises used: Set.Mem, convexAddSubmonoid, setOf, Convex, AddSubmonoid.multiset_sum_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ι : Type u_5
s : Finset ι
t : ι → Set E
h : ∀ i ∈ s, Convex 𝕜 (t i)
⊢ Convex.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, t i)

Tactic:
(convexAddSubmonoid 𝕜 E).sum_mem h

Premises used: Set.Mem, convexAddSubmonoid, setOf, Convex, AddSubmonoid.sum_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
simp_rw : Convex 𝕜 ({z} + s)
⊢ Convex 𝕜 (z +ᵥ s)

Tactic:
simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]

Premises used: Set.image_vadd, Set.singleton_add, vadd_eq_add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)

Tactic:
(convex_singleton _).add hs

Premises used: convex_singleton, Convex.add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)

Tactic:
exact (convex_singleton _).add hs

Premises used: convex_singleton, Convex.add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 (E := E) ((fun (x : E) ↦ z + x) '' s)

Tactic:
hs.vadd _

Premises used: Convex.vadd
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s

Tactic:
have h := hs hx hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₂ :
  ∀ (h : a • z + b • z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₃ :
  ∀ (h : (a + b) • z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₄ :
  ∀ (h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 z + (a • x + b • y) ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h : z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

Premises used: one_smul, add_smul, add_add_add_comm, smul_add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 (E := E) ((fun (x : E) ↦ x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.translate_preimage_right z

Premises used: Convex.translate_preimage_right, add_comm
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulMono 𝕜 β
r : β
⊢ Convex 𝕜 (Iic r)

Tactic:
fun x hx y hy a b ha hb hab =>
  calc
    a • x + b • y ≤ a • r + b • r :=
      add_le_add (smul_le_smul_of_nonneg_left hx ha) (smul_le_smul_of_nonneg_left hy hb)
    _ = r := Convex.combo_self hab _

Premises used: Trans.trans, Set.Mem, add_le_add, setOf, Convex.combo_self, Convex, Set.Iic, StarConvex, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulMono 𝕜 β
r : β
⊢ Convex 𝕜 (Ici r)

Tactic:
convex_Iic (β := βᵒᵈ) r

Premises used: convex_Iic, Set.Ici, setOf, OrderDual
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulMono 𝕜 β
r s : β
⊢ Convex 𝕜 (Icc r s)

Tactic:
Ici_inter_Iic.subst ((convex_Ici r).inter <| convex_Iic s)

Premises used: convex_Iic, Eq.subst, Convex.inter, convex_Ici, Set.Ici_inter_Iic
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w ≤ r}

Tactic:
(convex_Iic r).is_linear_preimage h

Premises used: convex_Iic, Set.Mem, setOf, Convex.is_linear_preimage, Set.preimage, Set.Iic
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | r ≤ f w}

Tactic:
(convex_Ici r).is_linear_preimage h

Premises used: Set.Ici, Set.Mem, setOf, Convex.is_linear_preimage, Set.preimage, convex_Ici
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
simp_rw : Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w ≤ r ∧ r ≤ f w}
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w = r}

Tactic:
simp_rw [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w ≤ r ∧ r ≤ f w}

Tactic:
(convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

Premises used: Set.Mem, setOf, convex_halfSpace_ge, Set.inter, Convex.inter, convex_halfSpace_le
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w ≤ r ∧ r ≤ f w}

Tactic:
exact (convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

Premises used: convex_halfSpace_ge, Convex.inter, convex_halfSpace_le
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
inr : ∀ (ha' : 0 < a), a • x + b • y ∈ Iio r
⊢ a • x + b • y ∈ Iio r

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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ b = 1

Tactic:
rw [zero_add] at hab

Premises used: zero_add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : 0 + b • y ∈ Iio r
inl₁ : b • y ∈ Iio r
inl₂ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 y ∈ Iio r
inl₃ inl₄ inl₅ inl₆ : y ∈ Iio r
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r

Tactic:
rwa [zero_smul, zero_add, hab, one_smul]

Premises used: zero_add, one_smul, zero_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
inr :
  ∀ (hx : x < r) ⦃y : β⦄ (hy : y < r) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (ha' : 0 < a),
    a • x + b • y ∈ Iio r
⊢ a • x + b • y ∈ Iio r

Tactic:
rw [mem_Iio] at hx hy

Premises used: Set.mem_Iio
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y < a • r + b • r

Tactic:
add_lt_add_of_lt_of_le
        (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)

Premises used: LT.lt.le, add_lt_add_of_lt_of_le, smul_lt_smul_of_pos_left, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • r + b • r = r

Tactic:
Convex.combo_self hab _

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Tactic:
calc
    a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le
        (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
    _ = r := Convex.combo_self hab _

Premises used: LT.lt.le, Convex.combo_self, add_lt_add_of_lt_of_le, smul_lt_smul_of_pos_left, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r : β
⊢ Convex 𝕜 (Ioi r)

Tactic:
convex_Iio (β := βᵒᵈ) r

Premises used: Set.Ioi, setOf, convex_Iio, OrderDual
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r s : β
⊢ Convex 𝕜 (Ioo r s)

Tactic:
Ioi_inter_Iio.subst ((convex_Ioi r).inter <| convex_Iio s)

Premises used: Eq.subst, Convex.inter, Set.Ioi_inter_Iio, convex_Iio, convex_Ioi
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r s : β
⊢ Convex 𝕜 (Ico r s)

Tactic:
Ici_inter_Iio.subst ((convex_Ici r).inter <| convex_Iio s)

Premises used: Set.Ici_inter_Iio, Eq.subst, Convex.inter, convex_Ici, convex_Iio
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r s : β
⊢ Convex 𝕜 (Ioc r s)

Tactic:
Ioi_inter_Iic.subst ((convex_Ioi r).inter <| convex_Iic s)

Premises used: Set.Ioi_inter_Iic, convex_Iic, Eq.subst, Convex.inter, convex_Ioi
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w < r}

Tactic:
(convex_Iio r).is_linear_preimage h

Premises used: Set.Mem, setOf, Convex.is_linear_preimage, Set.preimage, convex_Iio, Set.Iio
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | r < f w}

Tactic:
(convex_Ioi r).is_linear_preimage h

Premises used: Set.Ioi, Set.Mem, setOf, Convex.is_linear_preimage, Set.preimage, convex_Ioi
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : LinearOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulMono 𝕜 β
r s : β
⊢ Convex 𝕜 (uIcc r s)

Tactic:
convex_Icc _ _

Premises used: convex_Icc, Set.uIcc
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this : HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
suffices : HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
suffices (a • (1 : 𝕜)) • x + (b • (1 : 𝕜)) • y ∈ s by simpa using this
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1

Tactic:
simpa [add_smul] using congr($(hab) • (1 : 𝕜))

Premises used: add_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
refine_2 : 0 ≤ HSMul.hSMul (β := 𝕜) b 1
⊢ HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s

Tactic:
refine hs hx hy ?_ ?_ (by simpa [add_smul] using congr($(hab) • (1 : 𝕜)))
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ HSMul.hSMul (β := 𝕜) a 1

Tactic:
zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one

Premises used: smul_le_smul_of_nonneg_right, Eq.rec, zero_le_one, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ HSMul.hSMul (β := 𝕜) a 1

Tactic:
exact zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ HSMul.hSMul (β := 𝕜) b 1

Tactic:
zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one

Premises used: smul_le_smul_of_nonneg_right, Eq.rec, zero_le_one, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ HSMul.hSMul (β := 𝕜) b 1

Tactic:
exact zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}

Tactic:
fun x hx y hy _ _ ha hb hab =>
  ⟨hs hx.1 hy.1 ha hb hab,
    (hf (hs hx.1 hy.1 ha hb hab) (max_rec' (· ∈ s) hx.1 hy.1)
          (Convex.combo_le_max x y ha hb hab)).trans_lt
      (max_rec' (f · < r) hx.2 hy.2)⟩

Premises used: Set.Mem, setOf, Membership.mem, And.right, And.left, Convex, And.intro, LT.lt, Convex.combo_le_max, max_rec', LE.le.trans_lt, StarConvex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex 𝕜 s

Tactic:
hs

Premises used: OrderDual
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex 𝕜 s

Tactic:
exact hs
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x ≤ r}

Tactic:
MonotoneOn.convex_ge (β := βᵒᵈ) hf hs r

Premises used: MonotoneOn.convex_ge, setOf
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}

Tactic:
MonotoneOn.convex_gt (β := βᵒᵈ) hf hs r

Premises used: MonotoneOn.convex_gt, setOf