awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
rw :
  (↑q : Set E)ᶜ = preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)
⊢ (↑q : Set E)ᶜ =
    (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ

Tactic:
rw [prod_univ, LinearEquiv.image_eq_preimage_symm]

Premises used: Set.prod_univ, LinearEquiv.image_eq_preimage_symm
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
h :
  ∀ (x : E),
    x ∈ (↑q : Set E)ᶜ ↔
      Membership.mem (γ := Set E)
        (preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)) x
⊢ (↑q : Set E)ᶜ = preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
x : E
⊢ x ∈ (↑q : Set E)ᶜ ↔
    Membership.mem (γ := Set E)
      (preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)) x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
h :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        ((⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ) x ↔
      x ∈ image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
⊢ (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ =
    image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected (X := ↥p) {0}ᶜ
x : E
⊢ Membership.mem (γ := Set E)
      ((⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ) x ↔
    x ∈ image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)

Tactic:
simp [mem_add, and_assoc]

Premises used: and_assoc, Set.mem_add
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
simp_rw :
  image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ico 0 1)) =
    Ico x y
⊢ image (α := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → ℝ) (Ico 0 1) = Ico x y

Tactic:
simp_rw [Path.segment_apply, ← image_image _ Subtype.val (Ico 0 1)]

Premises used: Set.image_image, Set.Ico, OfNat.ofNat, Path.segment_apply, Subtype.val
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
simp : (fun (a : ℝ) ↦ a * (y - x) + x) '' Ico 0 1 = Ico x y
⊢ image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ico 0 1)) =
    Ico x y

Tactic:
simp only [lineMap_apply, vsub_eq_sub, smul_eq_mul, vadd_eq_add, image_subtype_val_Ico,
    Icc.coe_zero, Icc.coe_one]

Premises used: Set.Icc.coe_zero, Set.image_subtype_val_Ico, AffineMap.lineMap_apply, Set.Icc.coe_one, vadd_eq_add, smul_eq_mul, vsub_eq_sub
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
⊢ (fun (x_1 : ℝ) ↦ (y - x) * x_1 + x) '' Ico 0 1 = Ico ((y - x) * 0 + x) ((y - x) * 1 + x)

Tactic:
image_affine_Ico (sub_pos_of_lt h) x 0 1

Premises used: Set.image_affine_Ico, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) a → a * (y - x) + x = (y - x) * a + x
h₂ : x = (y - x) * 0 + x
h₃ : y = (y - x) * 1 + x
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ico 0 1 = Ico x y

Tactic:
convert! image_affine_Ico (sub_pos_of_lt h) x 0 1 using 2

Premises used: Set.image_affine_Ico, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
a : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Ico 0 1) a
⊢ a * (y - x) + x = (y - x) * a + x

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
simp_rw :
  image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ioc 0 1)) =
    Ioc x y
⊢ image (α := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → ℝ) (Ioc 0 1) = Ioc x y

Tactic:
simp_rw [Path.segment_apply, ← image_image _ Subtype.val (Ioc 0 1)]

Premises used: Set.image_image, Set.Ioc, OfNat.ofNat, Path.segment_apply, Subtype.val
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
simp : (fun (a : ℝ) ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y
⊢ image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ioc 0 1)) =
    Ioc x y

Tactic:
simp only [lineMap_apply, vsub_eq_sub, smul_eq_mul, vadd_eq_add, image_subtype_val_Ioc,
    Icc.coe_zero, Icc.coe_one]

Premises used: Set.Icc.coe_zero, AffineMap.lineMap_apply, Set.Icc.coe_one, vadd_eq_add, Set.image_subtype_val_Ioc, smul_eq_mul, vsub_eq_sub
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
⊢ (fun (x_1 : ℝ) ↦ (y - x) * x_1 + x) '' Ioc 0 1 = Ioc ((y - x) * 0 + x) ((y - x) * 1 + x)

Tactic:
image_affine_Ioc (sub_pos_of_lt h) x 0 1

Premises used: Set.image_affine_Ioc, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioc 0 1) a → a * (y - x) + x = (y - x) * a + x
h₂ : x = (y - x) * 0 + x
h₃ : y = (y - x) * 1 + x
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y

Tactic:
convert! image_affine_Ioc (sub_pos_of_lt h) x 0 1 using 2

Premises used: Set.image_affine_Ioc, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.PathConnected
Goal:
x y : ℝ
h : x < y
a : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Ioc 0 1) a
⊢ a * (y - x) + x = (y - x) * a + x

Tactic:
ring
-- 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
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g)

Tactic:
⟨convex_univ, fun x _ y _ a b ha hb hab ↦ ?_⟩

Premises used: convex_univ, And.intro, ConvexOn
-- 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
refine :
  ∀ (x : E),
    Membership.mem (γ := Set E) Set.univ x →
      ∀ (y : E),
        Membership.mem (γ := Set E) Set.univ y →
          ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
            (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
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g)

Tactic:
refine ⟨convex_univ, fun x _ y _ a b 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
inl :
  ∀ (hx : x ≤ 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
inr :
  ∀ (hx : e < x),
    (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
⊢ (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:
obtain hx | hx := le_or_gt x e

Premises used: le_or_gt
-- 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
inl :
  ∀ (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
inl₁ :
  ∀ (hy : e < 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
⊢ (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:
obtain hy | hy := le_or_gt y e

Premises used: le_or_gt
-- 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
inr :
  ∀ (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
inr₁ :
  ∀ (hy : e < 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
⊢ (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:
obtain hy | hy := le_or_gt y e

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

Tactic:
have hc : a • x + b • y ≤ e := (Convex.combo_le_max x y ha hb hab).trans (max_le hx hy)
-- 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 : y ≤ e
hc : a • x + b • y ≤ e
inl : f (a • x + b • y) ≤ a • f 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_mem (Set.Iic e) f g hx, Set.piecewise_eq_of_mem (Set.Iic e) f g hy,
      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 : x ≤ e
hy : y ≤ e
hc : a • x + b • y ≤ e
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
hf.2 hx hy ha hb hab

Premises used: 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 : x ≤ e
hy : y ≤ e
hc : a • x + b • y ≤ e
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
exact hf.2 hx hy ha hb hab

Premises used: 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 : x ≤ e
hy : e < y
inl : (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f 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 • (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_mem (Set.Iic e) f g hx,
      Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr 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 : x ≤ e
hy : e < y
inl : ∀ (hc : a • x + b • y ≤ e), (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • f x + b • g y
inl₁ : ∀ (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
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • f x + b • g 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 : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
inl : f (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_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 : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
bc : 0 ≤ b
⊢ a • x + b • e ≤ 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 : x ≤ e
hy : e < y
hc : a • x + b • y ≤ e
⊢ a • x + b • e ≤ a • x + b • y

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

Tactic:
trans a • f x + b • f 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 : 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 • f e

Tactic:
(h_anti (hc'.trans hc) hc hc').trans (hf.2 hx Set.self_mem_Iic 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 : 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 • f e

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

Premises used: Set.self_mem_Iic, And.right, LE.le.trans