awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Piecewise
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
rw : a • f x + b • g e ≤ a • f x + b • g y
⊢ a • f x + b • f e ≤ a • f x + b • g y

Tactic:
rw [h_eq]
-- Module: Mathlib.Analysis.Convex.Piecewise
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
bc : g e ≤ g y
⊢ a • f x + b • g e ≤ a • f x + b • g y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ g e ≤ g y

Tactic:
h_mono Set.self_mem_Ici hy.le hy.le

Premises used: LT.lt.le, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ g e ≤ g y

Tactic:
exact h_mono Set.self_mem_Ici hy.le hy.le

Premises used: LT.lt.le, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Convex.Piecewise
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
inl : g (a • x + b • y) ≤ a • f x + b • g y
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f 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)]

Premises used: Iff.mpr, Set.piecewise_eq_of_notMem, Set.notMem_Iic, Set.Iic
-- Module: Mathlib.Analysis.Convex.Piecewise
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
bc : 0 ≤ a
⊢ a • x + b • y ≤ a • e + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ a • x + b • y ≤ a • e + b • y

Tactic:
have hc' : a • x + b • y ≤ a • e + b • y := by gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
trans₁ : a • g e + b • g y ≤ a • f x + b • g y
⊢ g (a • x + b • y) ≤ a • f x + b • g y

Tactic:
trans a • g e + b • g y
-- Module: Mathlib.Analysis.Convex.Piecewise
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 • g e + b • g y

Tactic:
(h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.self_mem_Ici hy.le ha hb hab)

Premises used: LT.lt.le, And.right, LE.le.trans, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Convex.Piecewise
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 • g e + b • g y

Tactic:
exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 Set.self_mem_Ici hy.le ha hb hab)

Premises used: LT.lt.le, And.right, LE.le.trans, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Convex.Piecewise
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
rw : a • f e + b • g y ≤ a • f x + b • g y
⊢ a • g e + b • g y ≤ a • f x + b • g y

Tactic:
rw [← h_eq]
-- Module: Mathlib.Analysis.Convex.Piecewise
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
bc : f e ≤ f x
⊢ a • f e + b • g y ≤ a • f x + b • g y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ f e ≤ f x

Tactic:
h_anti hx Set.self_mem_Iic hx

Premises used: Set.self_mem_Iic
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ f e ≤ f x

Tactic:
exact h_anti hx Set.self_mem_Iic hx

Premises used: Set.self_mem_Iic
-- Module: Mathlib.Analysis.Convex.Piecewise
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 : (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 • (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g x + b • (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g 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]

Premises used: Iff.mpr, Set.piecewise_eq_of_notMem, Set.notMem_Iic, Set.piecewise_eq_of_mem, Set.Iic
-- Module: Mathlib.Analysis.Convex.Piecewise
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
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
⊢ (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

Premises used: le_or_gt, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Piecewise
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
inr : f (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

Tactic:
rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]

Premises used: Set.piecewise_eq_of_mem, Set.Iic
-- Module: Mathlib.Analysis.Convex.Piecewise
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
bc : 0 ≤ a
⊢ a • e + b • y ≤ a • x + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ a • e + b • y ≤ a • x + b • y

Tactic:
have hc' : a • e + b • y ≤ a • x + b • y := by gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
trans₁ : a • f e + b • f y ≤ a • g x + b • f y
⊢ f (a • x + b • y) ≤ a • g x + b • f y

Tactic:
trans a • f e + b • f y
-- Module: Mathlib.Analysis.Convex.Piecewise
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 • f e + b • f y

Tactic:
(h_anti (hc'.trans hc) hc hc').trans (hf.2 Set.self_mem_Iic hy ha hb hab)

Premises used: Set.self_mem_Iic, And.right, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Piecewise
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 • f e + b • f y

Tactic:
exact (h_anti (hc'.trans hc) hc hc').trans (hf.2 Set.self_mem_Iic hy ha hb hab)

Premises used: Set.self_mem_Iic, And.right, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Piecewise
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
rw : a • g e + b • f y ≤ a • g x + b • f y
⊢ a • f e + b • f y ≤ a • g x + b • f y

Tactic:
rw [h_eq]
-- Module: Mathlib.Analysis.Convex.Piecewise
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
bc : g e ≤ g x
⊢ a • g e + b • f y ≤ a • g x + b • f y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ g e ≤ g x

Tactic:
h_mono Set.self_mem_Ici hx.le hx.le

Premises used: LT.lt.le, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Convex.Piecewise
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
⊢ g e ≤ g x

Tactic:
exact h_mono Set.self_mem_Ici hx.le hx.le

Premises used: LT.lt.le, Set.self_mem_Ici