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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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₁ : f x ≤ max (f x) (g x)
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₂ : f y ≤ max (f y) (g y)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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 • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₁ : g x ≤ max (f x) (g x)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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₁ : g x ≤ max (f x) (g x)
⊢ a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₂ : g y ≤ max (f y) (g y)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)
have h₁ : f x ≤ max (f x) (f y)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : f x ≤ max (f x) (f y)
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)
have h₂ : f y ≤ max (f x) (f y)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)
have h₁ : f x ≤ max (f x) (f y)
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 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : f x ≤ max (f x) (f y)
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)
have h₂ : f y ≤ max (f x) (f y)
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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y
have rw : ∀ (hab : b + a = 1) (hfx : f x ≤ f (b • y + a • x)), f (b • y + a • x) ≤ f y
Tactic: rw [add_comm] at hab hfx ⊢
Cleared hypotheses: hab, hfx
-- 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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y ≤ f z
⊢ f z ≤ f x
have obtain : ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hyz : f y ≤ f (a • x + b • y)), f (a • x + b • y) ≤ f x
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
Cleared hypotheses: z, hz, hyz
-- 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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x ≤ f z
⊢ f z ≤ f y
have obtain : ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxz : f x ≤ f (a • x + b • y)), f (a • x + b • y) ≤ f y
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
Cleared hypotheses: z, hz, hxz
-- 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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y
have rw : ∀ (hab : b + a = 1) (hfx : f x < f (b • y + a • x)), f (b • y + a • x) < f y
Tactic: rw [add_comm] at hab hfx ⊢
Cleared hypotheses: hab, hfx
-- 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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y < f z
⊢ f z < f x
have obtain : ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hyz : f y < f (a • x + b • y)), f (a • x + b • y) < f x
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
Cleared hypotheses: z, hz, hyz
-- 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 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x < f z
⊢ f z < f y
have obtain : ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxz : f x < f (a • x + b • y)), f (a • x + b • y) < f y
Tactic: obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
Cleared hypotheses: z, hz, hxz
-- 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f
have mp : ConvexOn 𝕜 s (-f) → ConcaveOn 𝕜 s f
Tactic: constructor
-- 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
mp : ConvexOn 𝕜 s (-f) → ConcaveOn 𝕜 s f
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f
have mpr : ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)
Tactic: constructor
-- 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 : 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
⊢ ConcaveOn 𝕜 s f
have 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)
Tactic: refine ⟨hconv, fun 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 : 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)
have 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
Tactic: refine ⟨hconv, fun 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 : 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
⊢ (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
have mpr : -(a • (-f) x + b • (-f) y) ≤ -(-f) (a • x + b • y)
Tactic: rw [← neg_le_neg_iff]
-- 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 : 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)
have mpr : a • f x + b • f y ≤ f (a • x + b • y)
Tactic: simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
-- 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
have rw : ConvexOn 𝕜 s (- -f) ↔ ConvexOn 𝕜 s f
Tactic: rw [← neg_convexOn_iff, neg_neg f]
-- 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 : 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
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
have rw₁ : ConvexOn 𝕜 s f ↔ ConvexOn 𝕜 s f
Tactic: rw [← neg_convexOn_iff, neg_neg f]
-- 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f
have mp : StrictConvexOn 𝕜 s (-f) → StrictConcaveOn 𝕜 s f
Tactic: constructor
-- 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 : 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
⊢ StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f
have mpr : StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (-f)
Tactic: constructor
-- 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 : 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
have 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)
Tactic: refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
-- 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 : 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
⊢ a • f x + b • f y < f (a • x + b • y)
have 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)
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
Cleared hypotheses: h
-- 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 : 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)
have 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
Tactic: refine ⟨hconv, 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 : 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
⊢ (-f) (a • x + b • y) < a • (-f) x + b • (-f) y
have mpr : -(a • (-f) x + b • (-f) y) < -(-f) (a • x + b • y)
Tactic: rw [← neg_lt_neg_iff]
-- 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 : 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)
have mpr : a • f x + b • f y < f (a • x + b • y)
Tactic: simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
-- 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 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f
have rw : StrictConvexOn 𝕜 s (- -f) ↔ StrictConvexOn 𝕜 s f
Tactic: rw [← neg_strictConvexOn_iff, neg_neg f]
-- 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 : 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
⊢ StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f
have rw₁ : StrictConvexOn 𝕜 s f ↔ StrictConvexOn 𝕜 s f
Tactic: rw [← neg_strictConvexOn_iff, neg_neg f]
-- 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 : 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
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, 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 : 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))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₁ : f (c + (a • x + b • y)) = f (a • c + a • x + (b • c + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, 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 : 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))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₂ : f (c + (a • x + b • y)) = f (a • c + b • c + (a • x + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, 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 : 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))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₃ : f (c + (a • x + b • y)) = f (c + (a • x + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, 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 : 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
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y
have rw : c • a • f x + c • b • f y = a • c • f x + b • c • f y
Tactic: rw [smul_add, smul_comm c, smul_comm c]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y
have rw₁ : a • c • f x + c • b • f y = a • c • f x + b • c • f y
Tactic: rw [smul_add, smul_comm c, smul_comm c]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y
have rw₂ : a • c • f x + b • c • f y = a • c • f x + b • c • f y
Tactic: rw [smul_add, smul_comm c, smul_comm c]