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 : 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
mp :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConcaveOn 𝕜 s f

Tactic:
refine ⟨hconv, fun x hx y hy a b 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 : 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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
simpa [add_comm] using h hx hy ha hb hab

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 : 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 → a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConvexOn 𝕜 s (-f)

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

Premises used: 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 : 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 → a • f x + b • f y ≤ f (a • x + b • y)
mpr :
  ∀ (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)

Tactic:
refine ⟨hconv, fun x hx y hy a b 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 : 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 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
mpr : -(a • (-f) x + b • (-f) y) ≤ -(-f) (a • x + b • y)
⊢ (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y

Tactic:
rw [← neg_le_neg_iff]

Premises used: neg_le_neg_iff
-- 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 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
mpr : a • f x + b • f y ≤ f (a • x + b • y)
⊢ -(a • (-f) x + b • (-f) y) ≤ -(-f) (a • x + b • y)

Tactic:
simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]

Premises used: neg_add, neg_neg, smul_neg, Pi.neg_apply
-- 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 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
h 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 : 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 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
exact h 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
rw : ConvexOn 𝕜 s (- -f) ↔ ConvexOn 𝕜 s f
rw₁ rw₂ : ConvexOn 𝕜 s f ↔ ConvexOn 𝕜 s f
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

Tactic:
rw [← neg_convexOn_iff, neg_neg f]

Premises used: neg_convexOn_iff, neg_neg
-- 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 : StrictConvexOn 𝕜 s (-f) → StrictConcaveOn 𝕜 s f
mpr : StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (-f)
⊢ StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (-f) (a • x + b • y) < a • (-f) x + b • (-f) y
⊢ StrictConcaveOn 𝕜 s f

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

Premises used: StrictConcaveOn, 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 : 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (-f) (a • x + b • y) < a • (-f) x + b • (-f) y
mp :
  ∀ (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),
    a • f x + b • f y < f (a • x + b • y)
⊢ StrictConcaveOn 𝕜 s f

Tactic:
refine ⟨hconv, fun x hx y hy hxy a b 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 : 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 → x ≠ y → ∀ ⦃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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ¬x = y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)

Tactic:
simp only [ne_eq, Pi.neg_apply, smul_neg, lt_add_neg_iff_add_lt, add_comm,
      add_neg_lt_iff_lt_add] at h

Premises used: lt_add_neg_iff_add_lt, smul_neg, ne_eq, add_comm, Pi.neg_apply, add_neg_lt_iff_lt_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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
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 :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ¬x = y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
⊢ a • f x + b • f y < f (a • x + b • y)

Tactic:
h hx hy hxy 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
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 :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ¬x = y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
⊢ a • f x + b • f y < f (a • x + b • y)

Tactic:
exact h hx hy hxy 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 : 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
⊢ StrictConvexOn 𝕜 s (-f)

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

Premises used: StrictConvexOn, 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 : 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
mpr :
  ∀ (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) (a • x + b • y) < a • (-f) x + b • (-f) y
⊢ StrictConvexOn 𝕜 s (-f)

Tactic:
refine ⟨hconv, fun x hx y hy hxy a b 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 : 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
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
mpr : -(a • (-f) x + b • (-f) y) < -(-f) (a • x + b • y)
⊢ (-f) (a • x + b • y) < a • (-f) x + b • (-f) y

Tactic:
rw [← neg_lt_neg_iff]

Premises used: neg_lt_neg_iff
-- 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
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
mpr : a • f x + b • f y < f (a • x + b • y)
⊢ -(a • (-f) x + b • (-f) y) < -(-f) (a • x + b • y)

Tactic:
simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]

Premises used: neg_add, neg_neg, smul_neg, Pi.neg_apply
-- 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
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
⊢ a • f x + b • f y < f (a • x + b • y)

Tactic:
h hx hy hxy 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 : 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 → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
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
⊢ a • f x + b • f y < f (a • x + b • y)

Tactic:
exact h hx hy hxy 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
rw : StrictConvexOn 𝕜 s (- -f) ↔ StrictConvexOn 𝕜 s f
rw₁ rw₂ : StrictConvexOn 𝕜 s f ↔ StrictConvexOn 𝕜 s f
⊢ StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f

Tactic:
rw [← neg_strictConvexOn_iff, neg_neg f]

Premises used: neg_strictConvexOn_iff, neg_neg
-- 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
⊢ ConvexOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add hg.neg

Premises used: sub_eq_add_neg, Eq.rec, ConcaveOn.neg, ConvexOn.add, Eq.symm
-- 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 g : E → β
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ConcaveOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add hg.neg

Premises used: sub_eq_add_neg, Eq.rec, ConvexOn.neg, ConcaveOn.add, Eq.symm
-- 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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConcaveOn 𝕜 s g
⊢ StrictConvexOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add hg.neg

Premises used: sub_eq_add_neg, Eq.rec, StrictConvexOn.add, StrictConcaveOn.neg, Eq.symm
-- 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 g : E → β
hf : StrictConcaveOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add hg.neg

Premises used: StrictConvexOn.neg, sub_eq_add_neg, Eq.rec, StrictConcaveOn.add, Eq.symm
-- 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : StrictConcaveOn 𝕜 s g
⊢ StrictConvexOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add_strictConvexOn hg.neg

Premises used: sub_eq_add_neg, Eq.rec, ConvexOn.add_strictConvexOn, StrictConcaveOn.neg, Eq.symm
-- 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 g : E → β
hf : ConcaveOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add_strictConcaveOn hg.neg

Premises used: StrictConvexOn.neg, sub_eq_add_neg, Eq.rec, Eq.symm, ConcaveOn.add_strictConcaveOn
-- 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 g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
⊢ StrictConvexOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add_convexOn hg.neg

Premises used: sub_eq_add_neg, Eq.rec, ConcaveOn.neg, StrictConvexOn.add_convexOn, Eq.symm
-- 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 g : E → β
hf : StrictConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ StrictConcaveOn 𝕜 s (f - g)

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add_concaveOn hg.neg

Premises used: sub_eq_add_neg, Eq.rec, ConvexOn.neg, StrictConcaveOn.add_concaveOn, Eq.symm
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCancelCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ 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 : AddCancelCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
c : E
⊢ StrictConcaveOn 𝕜 (E := E) ((fun (z : E) ↦ c + z) ⁻¹' s) (f ∘ fun (z : E) ↦ c + z)

Tactic:
hf.dual.translate_right _

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

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

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

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

Premises used: StrictConcaveOn.translate_right, add_comm
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : PosSMulMono 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : c • a • f x + c • b • f y = a • c • f x + b • c • f y
rw₁ : a • c • f x + c • b • f y = a • c • f x + b • c • f y
rw₂ rw₃ : a • c • f x + b • c • f y = a • c • f x + b • c • f y
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y

Tactic:
rw [smul_add, smul_comm c, smul_comm c]

Premises used: SMulCommClass.smul_comm, smul_add
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : SMul 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : PosSMulMono 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConcaveOn 𝕜 s f
⊢ ConcaveOn.{u_1, u_2, u_5} 𝕜 (β := β) s fun (x : E) ↦ c • f x

Tactic:
hf.dual.smul hc

Premises used: ConvexOn.smul, ConcaveOn, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw rw₁ :
  f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
⊢ f ((g : (a : E) → F) (a • x + b • y)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))

Tactic:
rw [Convex.combo_affine_apply hab]

Premises used: Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConcaveOn 𝕜 s f
⊢ ConcaveOn.{u_1, u_2, u_5} 𝕜 (E := E) ((⇑g : (a : E) → F) ⁻¹' s) (f ∘ (⇑g : (a : E) → F))

Tactic:
hf.dual.comp_affineMap g

Premises used: ConvexOn.comp_affineMap, ConcaveOn, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
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 : 0 < a + b
apply : a / (a + b) + b / (a + b) = 1
⊢ f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
apply h hx hy (div_nonneg ha hab.le) (div_nonneg hb hab.le)

Premises used: LT.lt.le, div_nonneg