-- Mathlib/Analysis/Convex/Function.lean
theorem LinearOrder.convexOn_of_lt (hs : Convex 𝕜 s)
    (hf : ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, 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

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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 : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃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 ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → 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

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

Result:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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 : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃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 ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → 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

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
wlog h : x < y

Result:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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 : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃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 ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → 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

𝕜✝ : Type u_1
E✝ : Type u_2
β✝ : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜✝
inst✝¹⁰ : AddCommMonoid E✝
inst✝⁹ : OrderedAddCommMonoid β✝
inst✝⁸ : Module 𝕜✝ E✝
inst✝⁷ : Module 𝕜✝ β✝
inst✝⁶ : LinearOrder E✝
s✝ : Set E✝
f✝ : E✝ → β✝
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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 : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃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 ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → 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:
rw [add_comm] at hab

Result:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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 : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃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 ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → 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

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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:
refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : 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
⊢ f (a • x + b • y) ≤ a • f x + b • f y