awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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)
⊢ 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)
have inl₁ : f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
Tactic: simp_rw [zero_smul, zero_add, one_smul, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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)
⊢ 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)
have inl₂ : f y ≤ f y
Tactic: simp_rw [zero_smul, zero_add, one_smul, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have 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)
Tactic: obtain rfl | hb' := hb.eq_or_lt
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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)
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inr₁ : ∀ (hb' : 0 < b), f (a • x + b • y) ≤ a • f x + b • f y
Tactic: obtain rfl | hb' := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
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
⊢ 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)
have hab₁ : a = 1
Tactic: rw [add_zero] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ 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)
have 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)
Tactic: subst a
Cleared hypotheses: a, ha, ha', hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ 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)
have 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
Tactic: simp_rw [zero_smul, add_zero, one_smul, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ 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)
have inr₁ : f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f x)
Tactic: simp_rw [zero_smul, add_zero, one_smul, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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)
⊢ 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)
have inr₂ : f x ≤ f x
Tactic: simp_rw [zero_smul, add_zero, one_smul, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 ∧
      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
have 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
Tactic: rw [convexOn_iff_forall_pos]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
have 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
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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inl : ∀ (hy : x ∈ s), f (a • x + b • x) ≤ a • f x + b • f x
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inr : ∀ (hxy : x ≠ y), f (a • x + b • y) ≤ a • f x + b • f y
Tactic: obtain rfl | hxy := eq_or_ne x y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • x) ≤ a • f x + b • f x
have inl : f x ≤ a • f x + b • f x
Tactic: rw [Convex.combo_self hab, Convex.combo_self hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • x) ≤ a • f x + b • f x
have inl₁ : f x ≤ f x
Tactic: rw [Convex.combo_self hab, Convex.combo_self hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ (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 : β)
have 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 : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β)
⊢ (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 : β)
have 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 : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β)
⊢ (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 : β)
have 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 : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ 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)
have 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) : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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) : β)
⊢ 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)
have 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) : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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) : β)
⊢ 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)
have 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 : β)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a • f x + b • f y ≤ a • r + b • r
have h₁ : f x ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a • f x + b • f y ≤ a • r + b • r
have h₂ : f y ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
have 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
Tactic: refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have 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
Tactic: wlog h : x < y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have 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
Tactic: wlog h : x < y
Cleared hypotheses: hs, hf, x, hx, y, hy, hxy, a, b, ha, hb, hab