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 : 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 = 1
inr :
  ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 1) (ha' : LT.lt.{u_1} (α := 𝕜) 0 1),
    f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y) ≤
      HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f y)
⊢ 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)

Tactic:
subst a
-- 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
hb : LE.le.{u_1} (α := 𝕜) 0 0
ha : LE.le.{u_1} (α := 𝕜) 0 1
ha' : LT.lt.{u_1} (α := 𝕜) 0 1
inr : f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f x) + 0
inr₁ : f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f x)
inr₂ : f x ≤ f x
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f y)

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

Premises used: le_rfl, one_smul, zero_smul, add_zero
-- 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
hb' : 0 < b
⊢ f (a • x + b • y) ≤ a • f x + b • f 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 : 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
hb' : 0 < b
⊢ f (a • x + b • y) ≤ a • f x + b • f 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃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)

Tactic:
convexOn_iff_forall_pos (β := βᵒᵈ)

Premises used: convexOn_iff_forall_pos, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
rw :
  (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) ↔
    Convex 𝕜 s ∧
      s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [convexOn_iff_forall_pos]

Premises used: convexOn_iff_forall_pos
-- 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 → β
⊢ (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) ↔
    Convex 𝕜 s ∧
      s.Pairwise fun (x y : E) ↦ ∀ ⦃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 hb 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 :
  ∀ (h : s.Pairwise fun (x y : E) ↦ ∀ ⦃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
⊢ (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) ↔
    Convex 𝕜 s ∧
      s.Pairwise fun (x y : E) ↦ ∀ ⦃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 hb 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 : s.Pairwise fun (x y : E) ↦ ∀ ⦃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 : ∀ (hy : x ∈ s), f (a • x + b • x) ≤ a • f x + b • f x
inr : ∀ (hxy : x ≠ y), 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 | hxy := eq_or_ne x y

Premises used: eq_or_ne, 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 : s.Pairwise fun (x y : E) ↦ ∀ ⦃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
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
inl : f x ≤ a • f x + b • f x
inl₁ inl₂ : f x ≤ f x
⊢ f (a • x + b • x) ≤ a • f x + b • f x

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

Premises used: Convex.combo_self
-- 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 : s.Pairwise fun (x y : E) ↦ ∀ ⦃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
hxy : x ≠ y
⊢ f (a • x + b • y) ≤ a • f x + b • f 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃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
hxy : x ≠ y
⊢ f (a • x + b • y) ≤ a • f x + b • f 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
convexOn_iff_pairwise_pos (β := βᵒᵈ)

Premises used: ConcaveOn, convexOn_iff_pairwise_pos
-- 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 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x : E
h : x ∈ s
x_1 : E
h_1 : x_1 ∈ s
x_2 x_3 : 𝕜
h_2 : 0 ≤ x_2
h_3 : 0 ≤ x_3
h_4 : x_2 + x_3 = 1
rw :
  HAdd.hAdd (α := β) (β := β) ((f : (a : E) → β) (x_2 • x) : β) ((f : (a : E) → β) (x_3 • x_1) : β) ≤
    HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β)
rw₁ :
  HAdd.hAdd (β := β) (HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β)) ((f : (a : E) → β) (x_3 • x_1) : β) ≤
    HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β)
rw₂ rw₃ :
  HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β) ≤
    HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β)
⊢ (f : (a : E) → β) (x_2 • x + x_3 • x_1) ≤
    HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β)

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Premises used: LinearMap.map_add, LinearMap.map_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 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x : E
h : x ∈ s
x_1 : E
h_1 : x_1 ∈ s
x_2 x_3 : 𝕜
h_2 : 0 ≤ x_2
h_3 : 0 ≤ x_3
h_4 : x_2 + x_3 = 1
rw :
  HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β) ≤
    HAdd.hAdd (α := β) (β := β) ((f : (a : E) → β) (x_2 • x) : β) ((f : (a : E) → β) (x_3 • x_1) : β)
rw₁ :
  HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β) ≤
    HAdd.hAdd (β := β) (HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β)) ((f : (a : E) → β) (x_3 • x_1) : β)
rw₂ rw₃ :
  HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β) ≤
    HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β)
⊢ HSMul.hSMul (β := β) x_2 ((f : (a : E) → β) x : β) + HSMul.hSMul (β := β) x_3 ((f : (a : E) → β) x_1 : β) ≤
    (f : (a : E) → β) (x_2 • x + x_3 • x_1)

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Premises used: LinearMap.map_add, LinearMap.map_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 → β
hf : StrictConvexOn 𝕜 s f
⊢ ConvexOn 𝕜 s f

Tactic:
convexOn_iff_pairwise_pos.mpr
    ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab => (hf.2 hx hy hxy ha hb hab).le⟩

Premises used: Iff.mpr, LT.lt.le, And.right, And.left, And.intro, convexOn_iff_pairwise_pos
-- 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 → β
hf : StrictConcaveOn 𝕜 s f
⊢ ConcaveOn 𝕜 s f

Tactic:
hf.dual.convexOn

Premises used: StrictConvexOn.convexOn, StrictConcaveOn.dual, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
hx.2.le

Premises used: LT.lt.le, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
exact hx.2.le

Premises used: LT.lt.le, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
hy.2.le

Premises used: LT.lt.le, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 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
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
exact hy.2.le

Premises used: LT.lt.le, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : IsOrderedAddMonoid β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 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, StrictConvexOn.convex_lt, 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
⊢ ConvexOn 𝕜 s f

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

Premises used: Iff.mpr, And.intro, convexOn_iff_pairwise_pos
-- 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 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
refine :
  ∀ (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
⊢ ConvexOn 𝕜 s f

Tactic:
refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩

Premises used: Iff.mpr, And.intro, convexOn_iff_pairwise_pos
-- 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 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
inr :
  ∀
    (this :
      ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
        [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
        [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
        (hf :
          ∀ ⦃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)
        (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y)
    (h : ¬x < y), f (a • x + b • y) ≤ a • f x + b • f y
wlog :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
wlog h : x < y
-- 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 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
inr : f (b • y + a • x) ≤ b • f y + a • f x
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [add_comm (a • x), add_comm (a • f x)]

Premises used: add_comm, 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 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
⊢ b + a = 1

Tactic:
rw [add_comm] at 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
hab₁ : b + a = 1
⊢ ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [add_comm] at hab

Premises used: add_comm