awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b c d : E
hac : c = a
hbd : d = b
⊢ Eq (α := Path c d) (cast (Path.segment a b) hac hbd) (Path.segment c d)
have subst_vars : Eq (α := Path c d) (cast (Path.segment c d) sorry sorry) (Path.segment c d)
Tactic: subst_vars
Cleared hypotheses: a, b, hac, hbd
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
⊢ JoinedIn s x y
have h₁ : ∀ (t : (↑I : Type)), Membership.mem (α := E) s ((Path.segment x y : (a : (↑I : Type)) → E) t : E)
Tactic: use .segment x y
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
⊢ ∀ (t : (↑I : Type)), Membership.mem (α := E) s ((Path.segment x y : (a : (↑I : Type)) → E) t : E)
have h₁ : range (ι := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → E) ⊆ s
Tactic: rwa [← range_subset_iff, Path.range_segment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
⊢ IsPathConnected (↑q : Set E)ᶜ
have h : (↑q : Set E)ᶜ = image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
Tactic: convert! (hpc.image continuous_subtype_val).add q.isPathConnected using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
⊢ (↑q : Set E)ᶜ = image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
have trans : (↑q : Set E)ᶜ = (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ
Tactic: trans Submodule.prodEquivOfIsCompl p q hpq '' ({0}ᶜ ×ˢ univ)
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
trans :
  (↑q : Set E)ᶜ =
    (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ
⊢ (↑q : Set E)ᶜ = image (α := ↥p) (Subtype.val (p := fun (x : E) ↦ x ∈ p)) {0}ᶜ + (↑q : Set E)
have trans₁ : (⇑(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: trans Submodule.prodEquivOfIsCompl p q hpq '' ({0}ᶜ ×ˢ univ)
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
⊢ (↑q : Set E)ᶜ =
    (⇑(p.prodEquivOfIsCompl q hpq) : (a : ↥p × ↥q) → E) '' SProd.sprod (α := Set ↥p) (β := Set ↥q) {0}ᶜ univ
have rw : (↑q : Set E)ᶜ = preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)
Tactic: rw [prod_univ, LinearEquiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
⊢ (↑q : Set E)ᶜ = preimage (β := ↥p × ↥q) (⇑(p.prodEquivOfIsCompl q hpq).symm : (a : E) → ↥p × ↥q) (Prod.fst ⁻¹' {0}ᶜ)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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}ᶜ
⊢ (⇑(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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ image (α := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → ℝ) (Ico 0 1) = Ico x y
have simp_rw : image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
    (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ico 0 1)) =
  Ico x y
Tactic: simp_rw [Path.segment_apply, ← image_image _ Subtype.val (Ico 0 1)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ico 0 1)) =
    Ico x y
have simp : (fun (a : ℝ) ↦ a * (y - x) + x) '' 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ico 0 1 = Ico x y
have h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) a → a * (y - x) + x = (y - x) * a + x
Tactic: convert! image_affine_Ico (sub_pos_of_lt h) x 0 1 using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) a → a * (y - x) + x = (y - x) * a + x
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ico 0 1 = Ico x y
have h₂ : x = (y - x) * 0 + x
Tactic: convert! image_affine_Ico (sub_pos_of_lt h) x 0 1 using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ico 0 1 = Ico x y
have h₃ : y = (y - x) * 1 + x
Tactic: convert! image_affine_Ico (sub_pos_of_lt h) x 0 1 using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ image (α := (↑I : Type)) (⇑(Path.segment x y) : (a : (↑I : Type)) → ℝ) (Ioc 0 1) = Ioc x y
have simp_rw : image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
    (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ioc 0 1)) =
  Ioc x y
Tactic: simp_rw [Path.segment_apply, ← image_image _ Subtype.val (Ioc 0 1)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ image (α := ℝ) (⇑(lineMap x y) : (a : ℝ) → ℝ)
      (image (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Ioc 0 1)) =
    Ioc x y
have simp : (fun (a : ℝ) ↦ a * (y - x) + x) '' 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y
have h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioc 0 1) a → a * (y - x) + x = (y - x) * a + x
Tactic: convert! image_affine_Ioc (sub_pos_of_lt h) x 0 1 using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
x y : ℝ
h : x < y
h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioc 0 1) a → a * (y - x) + x = (y - x) * a + x
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y
have h₂ : x = (y - x) * 0 + x
Tactic: convert! image_affine_Ioc (sub_pos_of_lt h) x 0 1 using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
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
⊢ (fun (a : ℝ) ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y
have h₃ : y = (y - x) * 1 + x
Tactic: convert! image_affine_Ioc (sub_pos_of_lt h) x 0 1 using 2
-- 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
⊢ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g)
have 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
Tactic: refine ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ ?_⟩
-- 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
⊢ (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 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
Tactic: obtain hx | hx := le_or_gt x 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
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
⊢ (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 : ∀ (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
Tactic: obtain hx | hx := le_or_gt x 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
⊢ (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 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
Tactic: obtain hy | hy := le_or_gt 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 : 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
⊢ (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 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
Tactic: obtain hy | hy := le_or_gt 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
⊢ (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 : ∀ (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
Tactic: obtain hy | hy := le_or_gt 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
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
⊢ (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₁ : ∀ (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
Tactic: obtain hy | hy := le_or_gt y e
-- 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 : 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 hc : 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)
-- 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 : y ≤ e
hc : a • x + b • 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 inl : f (a • x + b • y) ≤ a • f x + b • f 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]
-- 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
⊢ (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 inl : (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 hx,
      Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr 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 : x ≤ e
hy : e < y
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • f x + b • g y
have 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
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 : 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
⊢ (Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g (a • x + b • y) ≤ a • f x + b • g y
have 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
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 : x ≤ e
hy : e < y
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
have inl : f (a • x + b • y) ≤ a • f x + b • g y
Tactic: rw [Set.piecewise_eq_of_mem (Set.Iic e) f g hc]