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 : e < x
hy : y ≤ e
hc : e < a • x + b • y
inr : 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:
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 : e < x
hy : y ≤ e
hc : e < a • x + b • y
bc : 0 ≤ b
⊢ a • x + b • y ≤ a • x + b • e

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 : e < a • x + b • y
⊢ a • x + b • y ≤ a • x + b • e

Tactic:
have hc' : a • x + b • y ≤ a • x + b • e := 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 : 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
trans₁ : a • g x + b • g e ≤ a • g x + b • f y
⊢ g (a • x + b • y) ≤ a • g x + b • f y

Tactic:
trans a • g x + b • g e
-- 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 : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ g (a • x + b • y) ≤ a • g x + b • g e

Tactic:
(h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 hx.le Set.self_mem_Ici 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 : 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 • g e

Tactic:
exact (h_mono hc.le (hc.le.trans hc') hc').trans (hg.2 hx.le Set.self_mem_Ici 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 : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
rw : a • g x + b • f e ≤ a • g x + b • f y
⊢ a • g x + b • g e ≤ 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 : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
bc : f e ≤ f y
⊢ a • g x + b • f e ≤ 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 : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ f e ≤ f y

Tactic:
h_anti hy Set.self_mem_Iic hy

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
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ f e ≤ f y

Tactic:
exact h_anti hy Set.self_mem_Iic hy

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 : e < y
⊢ e < a • x + b • y

Tactic:
have hc : e < a • x + b • y :=
        (lt_min hx hy).trans_le (Convex.min_le_combo x y ha hb hab)
-- 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 : e < y
hc : e < a • x + b • y
inr : g (a • x + b • y) ≤ a • g x + b • g 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.Iic e).piecewise_eq_of_notMem f g (Set.notMem_Iic.mpr hx),
      (Set.Iic e).piecewise_eq_of_notMem f g (Set.notMem_Iic.mpr hy),
      (Set.Iic e).piecewise_eq_of_notMem 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 : e < x
hy : e < y
hc : e < a • x + b • y
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
hg.2 hx.le hy.le ha hb hab

Premises used: LT.lt.le, And.right
-- 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 : e < y
hc : e < a • x + b • y
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
exact hg.2 hx.le hy.le ha hb hab

Premises used: LT.lt.le, And.right
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
h : ∀ (x : E), (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f

Tactic:
ext x
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
pos :
  ∀ (hx : x = e),
    (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
neg :
  ∀ (hx : ¬x = e),
    (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x

Tactic:
by_cases hx : x = e
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
hx : x = e
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x

Tactic:
simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]

Premises used: LE.le, le_iff_lt_or_eq, ite_not, Set.piecewise
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
hx : ¬x = e
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x

Tactic:
simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]

Premises used: LE.le, le_iff_lt_or_eq, ite_not, Set.piecewise
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f

Tactic:
have h_piecewise_Ici_eq_piecewise_Iic :
      (Set.Ici e).piecewise f g = (Set.Iic e).piecewise g f := by
    ext x; by_cases hx : x = e
      <;> simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
h_piecewise_Ici_eq_piecewise_Iic :
  (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f
rw : ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f)
⊢ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) f g)

Tactic:
rw [h_piecewise_Ici_eq_piecewise_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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
h_piecewise_Ici_eq_piecewise_Iic :
  (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f)

Tactic:
convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici hg hf h_anti h_mono h_eq.symm

Premises used: convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici, Eq.symm
-- 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.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
h_piecewise_Ici_eq_piecewise_Iic :
  (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f)

Tactic:
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici hg hf h_anti h_mono h_eq.symm

Premises used: convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici, Eq.symm
-- 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 : ConcaveOn 𝕜 (Set.Iic e) f
hg : ConcaveOn 𝕜 (Set.Ici e) g
h_mono : MonotoneOn f (Set.Iic e)
h_anti : AntitoneOn g (Set.Ici e)
h_eq : f e = g e
rw : ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))
⊢ ConcaveOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g)

Tactic:
rw [← neg_convexOn_iff, ← Set.piecewise_neg]

Premises used: neg_convexOn_iff, Set.piecewise_neg
-- 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 : ConcaveOn 𝕜 (Set.Iic e) f
hg : ConcaveOn 𝕜 (Set.Ici e) g
h_mono : MonotoneOn f (Set.Iic e)
h_anti : AntitoneOn g (Set.Ici e)
h_eq : f e = g e
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))

Tactic:
convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
    hf.neg hg.neg h_mono.neg h_anti.neg (neg_inj.mpr h_eq)

Premises used: Iff.mpr, AntitoneOn.neg, MonotoneOn.neg, convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici, neg_inj, ConcaveOn.neg
-- 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 : ConcaveOn 𝕜 (Set.Iic e) f
hg : ConcaveOn 𝕜 (Set.Ici e) g
h_mono : MonotoneOn f (Set.Iic e)
h_anti : AntitoneOn g (Set.Ici e)
h_eq : f e = g e
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))

Tactic:
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici
    hf.neg hg.neg h_mono.neg h_anti.neg (neg_inj.mpr h_eq)

Premises used: Iff.mpr, AntitoneOn.neg, MonotoneOn.neg, convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici, neg_inj, ConcaveOn.neg
-- 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 : ConcaveOn 𝕜 (Set.Ici e) f
hg : ConcaveOn 𝕜 (Set.Iic e) g
h_anti : AntitoneOn f (Set.Ici e)
h_mono : MonotoneOn g (Set.Iic e)
h_eq : f e = g e
rw : ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))
⊢ ConcaveOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) f g)

Tactic:
rw [← neg_convexOn_iff, ← Set.piecewise_neg]

Premises used: neg_convexOn_iff, Set.piecewise_neg
-- 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 : ConcaveOn 𝕜 (Set.Ici e) f
hg : ConcaveOn 𝕜 (Set.Iic e) g
h_anti : AntitoneOn f (Set.Ici e)
h_mono : MonotoneOn g (Set.Iic e)
h_eq : f e = g e
⊢ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))

Tactic:
convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic
    hf.neg hg.neg h_anti.neg h_mono.neg (neg_inj.mpr h_eq)

Premises used: Iff.mpr, AntitoneOn.neg, MonotoneOn.neg, convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic, neg_inj, ConcaveOn.neg