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 𝕜 β
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
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
⊢ ¬x < y

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

Tactic:
this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- 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 : b + a = 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
⊢ f (b • y + a • x) ≤ b • f y + a • f x

Tactic:
exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜_1 : Type u_1
E_1 : Type u_2
β_1 : Type u_5
inst : Semiring 𝕜_1
inst_1 : PartialOrder 𝕜_1
inst_2 : AddCommMonoid E_1
inst_3 : AddCommMonoid β_1
inst_4 : PartialOrder β_1
inst_5 : Module 𝕜_1 E_1
inst_6 : Module 𝕜_1 β_1
inst_7 : LinearOrder E_1
s_1 : Set E_1
f_1 : E_1 → β_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst_8 : Semiring 𝕜
inst_9 : PartialOrder 𝕜
inst_10 : AddCommMonoid E
inst_11 : AddCommMonoid β
inst_12 : PartialOrder β
inst_13 : Module 𝕜 E
inst_14 : Module 𝕜 β
inst_15 : 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:
hf hx hy h ha hb hab
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜_1 : Type u_1
E_1 : Type u_2
β_1 : Type u_5
inst : Semiring 𝕜_1
inst_1 : PartialOrder 𝕜_1
inst_2 : AddCommMonoid E_1
inst_3 : AddCommMonoid β_1
inst_4 : PartialOrder β_1
inst_5 : Module 𝕜_1 E_1
inst_6 : Module 𝕜_1 β_1
inst_7 : LinearOrder E_1
s_1 : Set E_1
f_1 : E_1 → β_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst_8 : Semiring 𝕜
inst_9 : PartialOrder 𝕜
inst_10 : AddCommMonoid E
inst_11 : AddCommMonoid β
inst_12 : PartialOrder β
inst_13 : Module 𝕜 E
inst_14 : Module 𝕜 β
inst_15 : 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:
exact hf hx hy h 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 𝕜 β
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 → a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConcaveOn 𝕜 s f

Tactic:
LinearOrder.convexOn_of_lt (β := βᵒᵈ) hs hf

Premises used: LinearOrder.convexOn_of_lt, 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 : 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
⊢ StrictConvexOn 𝕜 s f

Tactic:
⟨hs, 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 : 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
⊢ StrictConvexOn 𝕜 s f

Tactic:
refine ⟨hs, 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 : 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
-- 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
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
⊢ ¬x < y

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 : b + a = 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
⊢ f (b • y + a • x) < b • f y + a • f x

Tactic:
this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- 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 : b + a = 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
⊢ f (b • y + a • x) < b • f y + a • f x

Tactic:
exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜_1 : Type u_1
E_1 : Type u_2
β_1 : Type u_5
inst : Semiring 𝕜_1
inst_1 : PartialOrder 𝕜_1
inst_2 : AddCommMonoid E_1
inst_3 : AddCommMonoid β_1
inst_4 : PartialOrder β_1
inst_5 : Module 𝕜_1 E_1
inst_6 : Module 𝕜_1 β_1
inst_7 : LinearOrder E_1
s_1 : Set E_1
f_1 : E_1 → β_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst_8 : Semiring 𝕜
inst_9 : PartialOrder 𝕜
inst_10 : AddCommMonoid E
inst_11 : AddCommMonoid β
inst_12 : PartialOrder β
inst_13 : Module 𝕜 E
inst_14 : Module 𝕜 β
inst_15 : 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:
hf hx hy h ha hb hab
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜_1 : Type u_1
E_1 : Type u_2
β_1 : Type u_5
inst : Semiring 𝕜_1
inst_1 : PartialOrder 𝕜_1
inst_2 : AddCommMonoid E_1
inst_3 : AddCommMonoid β_1
inst_4 : PartialOrder β_1
inst_5 : Module 𝕜_1 E_1
inst_6 : Module 𝕜_1 β_1
inst_7 : LinearOrder E_1
s_1 : Set E_1
f_1 : E_1 → β_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst_8 : Semiring 𝕜
inst_9 : PartialOrder 𝕜
inst_10 : AddCommMonoid E
inst_11 : AddCommMonoid β
inst_12 : PartialOrder β
inst_13 : Module 𝕜 E
inst_14 : Module 𝕜 β
inst_15 : 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:
exact hf hx hy h 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 𝕜 β
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 → a • f x + b • f y < f (a • x + b • y)
⊢ StrictConcaveOn 𝕜 s f

Tactic:
LinearOrder.strictConvexOn_of_lt (β := βᵒᵈ) hs hf

Premises used: StrictConcaveOn, LinearOrder.strictConvexOn_of_lt
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] 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 :
  f (HAdd.hAdd (α := F) (β := F) ((g : (a : E) → F) (a • x) : F) ((g : (a : E) → F) (b • y) : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
rw₁ :
  f (HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F)) ((g : (a : E) → F) (b • y) : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
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 [g.map_add, g.map_smul, g.map_smul]

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

Tactic:
hf.dual.comp_linearMap g

Premises used: ConcaveOn, ConvexOn.comp_linearMap, ConcaveOn.dual