awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ max (f x) (f y)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ min (f x) (f y) ≤ f (a • x + b • y)

Tactic:
hf.dual.le_on_segment' hx hy ha hb hab

Premises used: ConvexOn.le_on_segment', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)

Tactic:
let ⟨_, _, ha, hb, hab, hz⟩ := hz
  hz ▸ hf.le_on_segment' hx hy ha hb hab

Premises used: Eq.rec, LE.le, Max.max, ConvexOn.le_on_segment', _private.0.ConvexOn.le_on_segment.match_1
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ min (f x) (f y) ≤ f z

Tactic:
hf.dual.le_on_segment hx hy hz

Premises used: ConvexOn.le_on_segment, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : f x ≤ max (f x) (f y)
h₂ : f y ≤ max (f x) (f y)
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ max (f x) (f y)

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ max (f x) (f y)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ min (f x) (f y) < f (a • x + b • y)

Tactic:
hf.dual.lt_on_open_segment' hx hy hxy ha hb hab

Premises used: StrictConvexOn.lt_on_open_segment', StrictConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hz : z ∈ openSegment 𝕜 x y
⊢ f z < max (f x) (f y)

Tactic:
let ⟨_, _, ha, hb, hab, hz⟩ := hz
  hz ▸ hf.lt_on_open_segment' hx hy hxy ha hb hab

Premises used: Eq.rec, Max.max, LT.lt, StrictConvexOn.lt_on_open_segment', _private.0.StrictConvexOn.lt_on_openSegment.match_1
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hz : z ∈ openSegment 𝕜 x y
⊢ min (f x) (f y) < f z

Tactic:
hf.dual.lt_on_openSegment hx hy hxy hz

Premises used: StrictConvexOn.lt_on_openSegment, StrictConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
hfy : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Tactic:
le_of_not_gt fun h ↦ lt_irrefl (f (a • x + b • y)) <|
    calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha.le hb hab
      _ < a • f (a • x + b • y) + b • f (a • x + b • y) := add_lt_add_of_lt_of_le
          (smul_lt_smul_of_pos_left h ha) (smul_le_smul_of_nonneg_left hfy hb)
      _ = f (a • x + b • y) := Convex.combo_self hab _

Premises used: Trans.trans, lt_irrefl, le_of_not_gt, LT.lt.le, Convex.combo_self, add_lt_add_of_lt_of_le, And.right, HAdd.hAdd, HSMul.hSMul, smul_lt_smul_of_pos_left, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
hfy : f (a • x + b • y) ≤ f y
⊢ f x ≤ f (a • x + b • y)

Tactic:
hf.dual.le_left_of_right_le' hx hy ha hb hab hfy

Premises used: ConvexOn.le_left_of_right_le', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
rw : ∀ (hab : b + a = 1) (hfx : f x ≤ f (b • y + a • x)), f (b • y + a • x) ≤ f y
⊢ f (a • x + b • y) ≤ f y

Tactic:
rw [add_comm] at hab hfx ⊢

Premises used: add_comm
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y

Tactic:
hf.le_left_of_right_le' hy hx hb ha hab hfx

Premises used: ConvexOn.le_left_of_right_le'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : b + a = 1
hfx : f x ≤ f (b • y + a • x)
⊢ f (b • y + a • x) ≤ f y

Tactic:
exact hf.le_left_of_right_le' hy hx hb ha hab hfx

Premises used: ConvexOn.le_left_of_right_le'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f (a • x + b • y) ≤ f x
⊢ f y ≤ f (a • x + b • y)

Tactic:
hf.dual.le_right_of_left_le' hx hy ha hb hab hfx

Premises used: ConvexOn.le_right_of_left_le', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y ≤ f z
obtain :
  ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hyz : f y ≤ f (a • x + b • y)), f (a • x + b • y) ≤ f x
⊢ f z ≤ f x

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Tactic:
hf.le_left_of_right_le' hx hy ha hb.le hab hyz

Premises used: ConvexOn.le_left_of_right_le', LT.lt.le
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Tactic:
exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz

Premises used: ConvexOn.le_left_of_right_le', LT.lt.le
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f z ≤ f y
⊢ f x ≤ f z

Tactic:
hf.dual.le_left_of_right_le hx hy hz hyz

Premises used: ConvexOn.le_left_of_right_le, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x ≤ f z
obtain :
  ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxz : f x ≤ f (a • x + b • y)), f (a • x + b • y) ≤ f y
⊢ f z ≤ f y

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
hf.le_right_of_left_le' hx hy ha.le hb hab hxz

Premises used: ConvexOn.le_right_of_left_le', LT.lt.le
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz

Premises used: ConvexOn.le_right_of_left_le', LT.lt.le
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f z ≤ f x
⊢ f y ≤ f z

Tactic:
hf.dual.le_right_of_left_le hx hy hz hxz

Premises used: ConvexOn.le_right_of_left_le, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfy : f y < f (a • x + b • y)
⊢ f (a • x + b • y) < f x

Tactic:
not_le.1 fun h ↦ lt_irrefl (f (a • x + b • y)) <|
    calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha.le hb.le hab
      _ < a • f (a • x + b • y) + b • f (a • x + b • y) := add_lt_add_of_le_of_lt
          (smul_le_smul_of_nonneg_left h ha.le) (smul_lt_smul_of_pos_left hfy hb)
      _ = f (a • x + b • y) := Convex.combo_self hab _

Premises used: not_le, add_lt_add_of_le_of_lt, Trans.trans, lt_irrefl, LT.lt.le, Convex.combo_self, And.right, HAdd.hAdd, Iff.mp, HSMul.hSMul, smul_lt_smul_of_pos_left, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfy : f (a • x + b • y) < f y
⊢ f x < f (a • x + b • y)

Tactic:
hf.dual.lt_left_of_right_lt' hx hy ha hb hab hfy

Premises used: ConvexOn.lt_left_of_right_lt', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f x < f (a • x + b • y)
rw : ∀ (hab : b + a = 1) (hfx : f x < f (b • y + a • x)), f (b • y + a • x) < f y
⊢ f (a • x + b • y) < f y

Tactic:
rw [add_comm] at hab hfx ⊢

Premises used: add_comm
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : b + a = 1
hfx : f x < f (b • y + a • x)
⊢ f (b • y + a • x) < f y

Tactic:
hf.lt_left_of_right_lt' hy hx hb ha hab hfx

Premises used: ConvexOn.lt_left_of_right_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : b + a = 1
hfx : f x < f (b • y + a • x)
⊢ f (b • y + a • x) < f y

Tactic:
exact hf.lt_left_of_right_lt' hy hx hb ha hab hfx

Premises used: ConvexOn.lt_left_of_right_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f (a • x + b • y) < f x
⊢ f y < f (a • x + b • y)

Tactic:
hf.dual.lt_right_of_left_lt' hx hy ha hb hab hfx

Premises used: ConvexOn.lt_right_of_left_lt', ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y < f z
obtain :
  ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hyz : f y < f (a • x + b • y)), f (a • x + b • y) < f x
⊢ f z < f x

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y < f (a • x + b • y)
⊢ f (a • x + b • y) < f x

Tactic:
hf.lt_left_of_right_lt' hx hy ha hb hab hyz

Premises used: ConvexOn.lt_left_of_right_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y < f (a • x + b • y)
⊢ f (a • x + b • y) < f x

Tactic:
exact hf.lt_left_of_right_lt' hx hy ha hb hab hyz

Premises used: ConvexOn.lt_left_of_right_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f z < f y
⊢ f x < f z

Tactic:
hf.dual.lt_left_of_right_lt hx hy hz hyz

Premises used: ConvexOn.lt_left_of_right_lt, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x < f z
obtain :
  ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxz : f x < f (a • x + b • y)), f (a • x + b • y) < f y
⊢ f z < f y

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
hf.lt_right_of_left_lt' hx hy ha hb hab hxz

Premises used: ConvexOn.lt_right_of_left_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
exact hf.lt_right_of_left_lt' hx hy ha hb hab hxz

Premises used: ConvexOn.lt_right_of_left_lt'
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f z < f x
⊢ f y < f z

Tactic:
hf.dual.lt_right_of_left_lt hx hy hz hxz

Premises used: ConvexOn.lt_right_of_left_lt, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
mp : ConvexOn 𝕜 s (-f) → ConcaveOn 𝕜 s f
mpr : ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
⊢ ConcaveOn 𝕜 s f

Tactic:
⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩

Premises used: And.intro, ConcaveOn