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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
rw₂ rw₃ : a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Premises used: add_add_add_comm, smul_add
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
⊢ StrictConvexOn 𝕜 s (f + g)

Tactic:
add_comm g f ▸ hg.add_convexOn hf

Premises used: Eq.rec, add_comm, StrictConvexOn.add_convexOn
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
rw₂ rw₃ : a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Premises used: add_add_add_comm, smul_add
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f + g)

Tactic:
hf.dual.add_convexOn hg.dual

Premises used: StrictConcaveOn, StrictConcaveOn.dual, StrictConvexOn.add_convexOn, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConcaveOn 𝕜 s f
hg : StrictConcaveOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f + g)

Tactic:
hf.dual.add_strictConvexOn hg.dual

Premises used: StrictConcaveOn, ConvexOn.add_strictConvexOn, StrictConcaveOn.dual, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConcaveOn 𝕜 s f
hg : StrictConcaveOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f + g)

Tactic:
hf.dual.add hg

Premises used: StrictConcaveOn, StrictConvexOn.add, StrictConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
γ : Type u_7
f : E → γ
inst_4 : AddCommMonoid γ
inst_5 : PartialOrder γ
inst_6 : IsOrderedCancelAddMonoid γ
inst_7 : Module 𝕜 γ
hf : StrictConvexOn 𝕜 s f
b : γ
⊢ StrictConvexOn 𝕜 s (f + fun (x : E) ↦ b)

Tactic:
hf.add_convexOn (convexOn_const _ hf.1)

Premises used: And.left, StrictConvexOn.add_convexOn, convexOn_const
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
γ : Type u_7
f : E → γ
inst_4 : AddCommMonoid γ
inst_5 : PartialOrder γ
inst_6 : IsOrderedCancelAddMonoid γ
inst_7 : Module 𝕜 γ
hf : StrictConcaveOn 𝕜 s f
b : γ
⊢ StrictConcaveOn 𝕜 s (f + fun (x : E) ↦ b)

Tactic:
hf.add_concaveOn (concaveOn_const _ hf.1)

Premises used: And.left, StrictConcaveOn.add_concaveOn, concaveOn_const
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}

Tactic:
convex_iff_forall_pos.2 fun x hx y hy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha.le hb.le hab
        _ < a • r + b • r :=
          (add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left hx.2 ha)
            (smul_le_smul_of_nonneg_left hy.2.le hb.le))
        _ = r := Convex.combo_self hab _⟩

Premises used: Iff.mpr, Trans.trans, LT.lt.le, Convex.combo_self, add_lt_add_of_lt_of_le, And.right, And.left, And.intro, smul_lt_smul_of_pos_left, convex_iff_forall_pos, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ r < f x}

Tactic:
hf.dual.convex_lt r

Premises used: setOf, ConvexOn.convex_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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} (a • p + b • q)

Tactic:
⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩

Premises used: Set.Mem, setOf, LT.lt.le, And.left, And.intro
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
refine : f (a • p + b • q).1 < (a • p + b • q).2
⊢ Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} (a • p + b • q)

Tactic:
refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1

Tactic:
hf.2 hp.1 hq.1 ha.le hb.le hab

Premises used: LT.lt.le, And.right, And.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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f p.1 + b • f q.1 < a • p.2 + b • q.2

Tactic:
add_lt_add_of_lt_of_le
       (smul_lt_smul_of_pos_left hp.2 ha) (smul_le_smul_of_nonneg_left hq.2 hb.le)

Premises used: LT.lt.le, add_lt_add_of_lt_of_le, And.right, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).1 < (a • p + b • q).2

Tactic:
calc
    f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1 := hf.2 hp.1 hq.1 ha.le hb.le hab
    _ < a • p.2 + b • q.2 := add_lt_add_of_lt_of_le
       (smul_lt_smul_of_pos_left hp.2 ha) (smul_le_smul_of_nonneg_left hq.2 hb.le)

Premises used: LT.lt.le, Prod.fst, add_lt_add_of_lt_of_le, And.right, And.left, HAdd.hAdd, HSMul.hSMul, smul_lt_smul_of_pos_left, Prod.snd, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ p.2 < f p.1
hq : q.1 ∈ s ∧ q.2 ≤ f q.1
⊢ openSegment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ p.2 < f p.1}

Tactic:
hf.dual.openSegment_subset_strict_epigraph p q hp hq

Premises used: Set.Mem, setOf, ConvexOn.openSegment_subset_strict_epigraph, OrderDual, 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
inst_9 : ZeroLEOneClass 𝕜
hf : ConvexOn 𝕜 s f
⊢ Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ f p.1 < p.2}

Tactic:
convex_iff_openSegment_subset.mpr fun p hp q hq =>
    hf.openSegment_subset_strict_epigraph p q hp ⟨hq.1, hq.2.le⟩

Premises used: Iff.mpr, convex_iff_openSegment_subset, ConvexOn.openSegment_subset_strict_epigraph, LT.lt.le, And.right, And.left, And.intro
-- 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 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
inst_9 : ZeroLEOneClass 𝕜
hf : ConcaveOn 𝕜 s f
⊢ Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ p.2 < f p.1}

Tactic:
hf.dual.convex_strict_epigraph

Premises used: Set.Mem, setOf, ConvexOn.convex_strict_epigraph, OrderDual, 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ConvexOn 𝕜 s (f ⊔ g)

Tactic:
⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩

Premises used: And.left, And.intro, sup_le, ConvexOn
-- 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
refine_1 :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
refine_2 :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
⊢ ConvexOn 𝕜 s (f ⊔ g)

Tactic:
refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
hf.right hx hy ha hb hab

Premises used: And.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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : f x ≤ max (f x) (g x)
h₂ : f y ≤ max (f y) (g y)
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ max (f x) (g x)

Tactic:
apply le_sup_left

Premises used: le_sup_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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ max (f y) (g y)

Tactic:
apply le_sup_left

Premises used: le_sup_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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
f₁ : a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
⊢ f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left

Premises used: And.right, HAdd.hAdd, Max.max, HSMul.hSMul
-- 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
hg.right hx hy ha hb hab

Premises used: And.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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : g x ≤ max (f x) (g x)
h₂ : g y ≤ max (f y) (g y)
⊢ a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g x ≤ max (f x) (g x)

Tactic:
apply le_sup_right

Premises used: le_sup_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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g y ≤ max (f y) (g y)

Tactic:
apply le_sup_right

Premises used: le_sup_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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
g₁ : a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
calc
      g (a • x + b • y) ≤ a • g x + b • g y := hg.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right

Premises used: And.right, HAdd.hAdd, Max.max, HSMul.hSMul
-- 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 g : E → β
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
⊢ ConcaveOn 𝕜 s (f ⊓ g)

Tactic:
hf.dual.sup hg

Premises used: ConvexOn.sup, ConcaveOn, 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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : f x ≤ max (f x) (g x)
h₂ : f y ≤ max (f y) (g y)
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g 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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ max (f x) (g x)

Tactic:
apply le_sup_left

Premises used: le_sup_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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ max (f y) (g y)

Tactic:
apply le_sup_left

Premises used: le_sup_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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : g x ≤ max (f x) (g x)
h₂ : g y ≤ max (f y) (g y)
⊢ a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g 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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g x ≤ max (f x) (g x)

Tactic:
apply le_sup_right

Premises used: le_sup_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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g y ≤ max (f y) (g y)

Tactic:
apply le_sup_right

Premises used: le_sup_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 g : E → β
hf : StrictConcaveOn 𝕜 s f
hg : StrictConcaveOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f ⊓ g)

Tactic:
hf.dual.sup hg

Premises used: StrictConcaveOn, StrictConvexOn.sup, 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 : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
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 : 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 x ≤ max (f x) (f y)

Tactic:
apply le_max_left

Premises used: le_max_left