awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : StrictConvexOn 𝕜 s f
hg' : StrictMonoOn g (f '' s)
hf' : InjOn f s
⊢ StrictConvexOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
    (hg' (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab)
            (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab) <|
          hf.2 hx hy hxy ha hb hab).trans <|
      hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab⟩

Premises used: StrictConvexOn, mt, LT.lt.le, And.right, And.left, Set.mem_image_of_mem, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConcaveOn 𝕜 (f '' s) g
hf : StrictConcaveOn 𝕜 s f
hg' : StrictMonoOn g (f '' s)
hf' : InjOn f s
⊢ StrictConcaveOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
    (hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab).trans <|
      hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab)
          (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab) <|
        hf.2 hx hy hxy ha hb hab⟩

Premises used: StrictConcaveOn, mt, LT.lt.le, And.right, And.left, Set.mem_image_of_mem, And.intro, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : StrictConcaveOn 𝕜 s f
hg' : StrictAntiOn g (f '' s)
hf' : InjOn f s
⊢ StrictConvexOn 𝕜 s (g ∘ f)

Tactic:
hg.dual.comp hf hg' hf'

Premises used: StrictConcaveOn.comp, StrictConvexOn, StrictConvexOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid α
inst_4 : PartialOrder α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 E
inst_8 : SMul 𝕜 α
inst_9 : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConcaveOn 𝕜 (f '' s) g
hf : StrictConvexOn 𝕜 s f
hg' : StrictAntiOn g (f '' s)
hf' : InjOn f s
⊢ StrictConcaveOn 𝕜 s (g ∘ f)

Tactic:
hg.dual.comp hf hg' hf'

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

Tactic:
hf.dual.add hg

Premises used: ConcaveOn, ConvexOn.add, 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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
c : β
hs : Convex 𝕜 s
⊢ ConvexOn.{u_1, u_2, u_5} 𝕜 (β := β) s fun (x : E) ↦ c

Tactic:
⟨hs, fun _ _ _ _ _ _ _ _ hab => (Convex.combo_self hab c).ge⟩

Premises used: Eq.ge, Convex.combo_self, And.intro, 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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
c : β
hs : Convex 𝕜 s
⊢ ConcaveOn.{u_1, u_2, u_5} 𝕜 (β := β) s fun (x : E) ↦ c

Tactic:
convexOn_const (β := βᵒᵈ) _ hs

Premises used: ConcaveOn, convexOn_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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
inst_7 : IsOrderedAddMonoid β
hf : ConvexOn 𝕜 s f
b : β
⊢ ConvexOn 𝕜 s (f + fun (x : E) ↦ b)

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

Premises used: And.left, ConvexOn.add, convexOn_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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
inst_7 : IsOrderedAddMonoid β
hf : ConcaveOn 𝕜 s f
b : β
⊢ ConcaveOn 𝕜 s (f + fun (x : E) ↦ b)

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

Premises used: ConcaveOn.add, And.left, 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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
h : Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}
⊢ ConvexOn 𝕜 s f

Tactic:
⟨fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).1,
    fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).2⟩

Premises used: le_rfl, And.right, And.left, And.intro, 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 : SMul 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
h : Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}
⊢ ConcaveOn 𝕜 s f

Tactic:
convexOn_of_convex_epigraph (β := βᵒᵈ) h

Premises used: convexOn_of_convex_epigraph, ConcaveOn
-- 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : f x ≤ r
h₂ : f y ≤ r
⊢ a • f x + b • f y ≤ a • r + b • r

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
hx.2

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
exact hx.2

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
hy.2

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
exact hy.2

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
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_le r

Premises used: setOf, ConvexOn.convex_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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).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 • (x, r) + b • (y, t))

Tactic:
⟨hf.1 hx hy ha hb hab, ?_⟩

Premises used: Set.Mem, setOf, 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine : f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2
⊢ Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (a • (x, r) + b • (y, t))

Tactic:
refine ⟨hf.1 hx hy ha hb 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
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.2 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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : 0 ≤ a
h₂ : 0 ≤ b
⊢ a • f x + b • f y ≤ a • r + b • t

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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
f₁ : a • f x + b • f y ≤ a • r + b • t
⊢ f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2

Tactic:
calc
    f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
    _ ≤ a • r + b • t := by gcongr

Premises used: And.right, HAdd.hAdd, 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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
⊢ Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}

Tactic:
hf.dual.convex_epigraph

Premises used: Set.Mem, setOf, ConvexOn.convex_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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔ Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
⟨ConvexOn.convex_epigraph, convexOn_of_convex_epigraph⟩

Premises used: ConvexOn.convex_epigraph, convexOn_of_convex_epigraph, Iff.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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f ↔ Convex 𝕜 (E := E × β) {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}

Tactic:
convexOn_iff_convex_epigraph (β := βᵒᵈ)

Premises used: Set.Mem, setOf, OrderDual, ConcaveOn, convexOn_iff_convex_epigraph
-- 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 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
rw₁ : f (c + (a • x + b • y)) = f (a • c + a • x + (b • c + b • y))
rw₂ : f (c + (a • x + b • y)) = f (a • c + b • c + (a • x + b • y))
rw₃ rw₄ : f (c + (a • x + b • y)) = f (c + (a • x + b • y))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]

Premises used: Convex.combo_self, 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 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
c : E
⊢ ConcaveOn 𝕜 (E := E) ((fun (z : E) ↦ c + z) ⁻¹' s) (f ∘ fun (z : E) ↦ c + z)

Tactic:
hf.dual.translate_right _

Premises used: ConvexOn.translate_right, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c : E
⊢ ConvexOn 𝕜 (E := E) ((fun (z : E) ↦ c + z) ⁻¹' s) (f ∘ fun (z : E) ↦ z + c)

Tactic:
simpa only [add_comm c] using hf.translate_right c

Premises used: ConvexOn.translate_right, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
c : E
⊢ ConcaveOn 𝕜 (E := E) ((fun (z : E) ↦ c + z) ⁻¹' s) (f ∘ fun (z : E) ↦ z + c)

Tactic:
hf.dual.translate_left _

Premises used: ConvexOn.translate_left, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃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

Tactic:
and_congr_right'
    ⟨fun h x hx y hy a b ha hb hab => h hx hy ha.le hb.le hab, fun h x hx y hy a b ha hb hab => ?_⟩

Premises used: and_congr_right', LT.lt.le, Iff.intro, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
refine :
  ∀
    (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)
    (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
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃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

Tactic:
refine and_congr_right'
    ⟨fun h x hx y hy a b ha hb hab => h hx hy ha.le hb.le hab, fun h x hx y hy a b ha hb hab => ?_⟩

Premises used: and_congr_right', Iff.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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl :
  ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1),
    f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y
inr : ∀ (ha' : 0 < a), f (a • x + b • y) ≤ a • f x + b • f y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

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

Premises used: LE.le.eq_or_lt, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
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.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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl :
  ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 1),
    f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤
      HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y

Tactic:
subst b
-- 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
ha : LE.le.{u_1} (α := 𝕜) 0 0
hb : LE.le.{u_1} (α := 𝕜) 0 1
inl : f (0 + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤ 0 + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
inl₁ : f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
inl₂ : f y ≤ f y
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)

Tactic:
simp_rw [zero_smul, zero_add, one_smul, le_rfl]

Premises used: le_rfl, zero_add, one_smul, zero_smul
-- 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
inr :
  ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1),
    f (a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y) ≤ a • f x + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f y)
inr₁ : ∀ (hb' : 0 < b), f (a • x + b • y) ≤ a • f x + b • f y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

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

Premises used: LE.le.eq_or_lt, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a = 1

Tactic:
rw [add_zero] at hab

Premises used: add_zero