awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
⊢ f (a • x + b • y) ≤ a • f x + b • g y
have hc' : a • x + b • e ≤ a • x + b • y
Tactic: have hc' : a • x + b • e ≤ a • x + b • y := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
hc' : a • x + b • e ≤ a • x + b • y
⊢ f (a • x + b • y) ≤ a • f x + b • g y
have trans : f (a • x + b • y) ≤ a • f x + b • f e
Tactic: trans a • f x + b • f e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
hc' : a • x + b • e ≤ a • x + b • y
trans : f (a • x + b • y) ≤ a • f x + b • f e
⊢ f (a • x + b • y) ≤ a • f x + b • g y
have trans₁ : a • f x + b • f e ≤ a • f x + b • g y
Tactic: trans a • f x + b • f e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
hc' : a • x + b • e ≤ a • x + b • y
⊢ a • f x + b • f e ≤ a • f x + b • g y
have rw : a • f x + b • g e ≤ a • f x + b • g y
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
hc' : a • x + b • e ≤ a • x + b • y
⊢ a • f x + b • g e ≤ a • f x + b • g y
have bc : g e ≤ g y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • f x + b • g y
have inl : g (a • x + b • y) ≤ a • f x + b • g y
Tactic: rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ g (a • x + b • y) ≤ a • f x + b • g y
have hc' : a • x + b • y ≤ a • e + b • y
Tactic: have hc' : a • x + b • y ≤ a • e + b • y := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ g (a • x + b • y) ≤ a • f x + b • g y
have trans : g (a • x + b • y) ≤ a • g e + b • g y
Tactic: trans a • g e + b • g y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
trans : g (a • x + b • y) ≤ a • g e + b • g y
⊢ g (a • x + b • y) ≤ a • f x + b • g y
have trans₁ : a • g e + b • g y ≤ a • f x + b • g y
Tactic: trans a • g e + b • g y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ a • g e + b • g y ≤ a • f x + b • g y
have rw : a • f e + b • g y ≤ a • f x + b • g y
Tactic: rw [← h_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • e + b • y
⊢ a • f e + b • g y ≤ a • f x + b • g y
have bc : f e ≤ f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤
    a • (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g x + b • (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g y
have inr : (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
Tactic: rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hx),
      Set.piecewise_eq_of_mem (Set.Iic e) f g hy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
have inr : ∀ (hc : a • x + b • y ≤ e), (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
Tactic: obtain hc | hc := le_or_gt (a • x + b • y) e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
inr : ∀ (hc : a • x + b • y ≤ e), (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
have inr₁ : ∀ (hc : e < a • x + b • y), (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
Tactic: obtain hc | hc := le_or_gt (a • x + b • y) e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
have inr : f (a • x + b • y) ≤ a • g x + b • f y
Tactic: rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
⊢ f (a • x + b • y) ≤ a • g x + b • f y
have hc' : a • e + b • y ≤ a • x + b • y
Tactic: have hc' : a • e + b • y ≤ a • x + b • y := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ f (a • x + b • y) ≤ a • g x + b • f y
have trans : f (a • x + b • y) ≤ a • f e + b • f y
Tactic: trans a • f e + b • f y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
trans : f (a • x + b • y) ≤ a • f e + b • f y
⊢ f (a • x + b • y) ≤ a • g x + b • f y
have trans₁ : a • f e + b • f y ≤ a • g x + b • f y
Tactic: trans a • f e + b • f y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ a • f e + b • f y ≤ a • g x + b • f y
have rw : a • g e + b • f y ≤ a • g x + b • f y
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : a • x + b • y ≤ e
hc' : a • e + b • y ≤ a • x + b • y
⊢ a • g e + b • f y ≤ a • g x + b • f y
have bc : g e ≤ g x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • g x + b • f y
have inr : g (a • x + b • y) ≤ a • g x + b • f y
Tactic: rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
⊢ g (a • x + b • y) ≤ a • g x + b • f y
have hc' : a • x + b • y ≤ a • x + b • e
Tactic: have hc' : a • x + b • y ≤ a • x + b • e := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ g (a • x + b • y) ≤ a • g x + b • f y
have trans : g (a • x + b • y) ≤ a • g x + b • g e
Tactic: trans a • g x + b • g e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
trans : g (a • x + b • y) ≤ a • g x + b • g e
⊢ g (a • x + b • y) ≤ a • g x + b • f y
have trans₁ : a • g x + b • g e ≤ a • g x + b • f y
Tactic: trans a • g x + b • g e
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ a • g x + b • g e ≤ a • g x + b • f y
have rw : a • g x + b • f e ≤ a • g x + b • f y
Tactic: rw [← h_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ a • g x + b • f e ≤ a • g x + b • f y
have bc : f e ≤ f y
Tactic: gcongr