awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
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 hc : 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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Piecewise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
inst_7 : AddCommGroup β
inst_8 : PartialOrder β
inst_9 : IsOrderedAddMonoid β
inst_10 : Module 𝕜 β
inst_11 : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
h : Membership.mem (γ := Set E) Set.univ x
y : E
h_1 : Membership.mem (γ := Set E) Set.univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : e < y
hc : e < a • x + b • 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 : g (a • x + b • y) ≤ a • g x + b • 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)]
-- 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.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
have h : ∀ (x : E), (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
Tactic: ext x
-- 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.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
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
have pos : ∀ (hx : x = e), (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
-- 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.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
⊢ (Set.Ici e).piecewise (β := fun (i : E) ↦ β) f g x = (Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f x
have neg : ∀ (hx : ¬x = e), (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
-- 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.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
⊢ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) f g)
have h_piecewise_Ici_eq_piecewise_Iic : (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]
-- 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.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.Ici e).piecewise (β := fun (a : E) ↦ β) f g)
have rw : ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (i : E) ↦ β) g f)
Tactic: rw [h_piecewise_Ici_eq_piecewise_Iic]
-- 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 : 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
⊢ ConcaveOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) f g)
have rw : ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))
Tactic: rw [← neg_convexOn_iff, ← Set.piecewise_neg]
-- 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 : 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
⊢ ConcaveOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) f g)
have rw : ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise (β := fun (a : E) ↦ β) (-f) (-g))
Tactic: rw [← neg_convexOn_iff, ← Set.piecewise_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst_4 : LinearOrder β
inst_5 : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) {x : E | x ∈ s ∧ (g ∘ f) x ≤ c} (a • x + b • y)
have simp : a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic: simp only [Function.comp_apply, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst_4 : LinearOrder β
inst_5 : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
have inr : ∀
  (this :
    ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_6 : PartialOrder 𝕜] [inst_7 : AddCommMonoid E]
      [inst_8 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_9 : LinearOrder β] [inst_10 : Preorder γ] {s : Set E}
      {f : E → β} {g : β → γ} (hg : Monotone g) (hf : QuasiconvexOn 𝕜 s f) (c : γ) (x : E) (hx : x ∈ s ∧ g (f x) ≤ c)
      (y : E) (hy : y ∈ s ∧ g (f y) ≤ c) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h : f x ≤ f y),
      a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c)
  (h : ¬f x ≤ f y), a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic: wlog h : f x ≤ f y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst_4 : LinearOrder β
inst_5 : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inr :
  ∀
    (this :
      ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_6 : PartialOrder 𝕜] [inst_7 : AddCommMonoid E]
        [inst_8 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_9 : LinearOrder β] [inst_10 : Preorder γ] {s : Set E}
        {f : E → β} {g : β → γ} (hg : Monotone g) (hf : QuasiconvexOn 𝕜 s f) (c : γ) (x : E) (hx : x ∈ s ∧ g (f x) ≤ c)
        (y : E) (hy : y ∈ s ∧ g (f y) ≤ c) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h : f x ≤ f y),
        a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c)
    (h : ¬f x ≤ f y), a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
have wlog : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_6 : PartialOrder 𝕜] [inst_7 : AddCommMonoid E]
  [inst_8 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_9 : LinearOrder β] [inst_10 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ} (hg : Monotone g) (hf : QuasiconvexOn 𝕜 s f) (c : γ) (x : E) (hx : x ∈ s ∧ g (f x) ≤ c)
  (y : E) (hy : y ∈ s ∧ g (f y) ≤ c) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h : f x ≤ f y),
  a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic: wlog h : f x ≤ f y
Cleared hypotheses: hg, hf, c, x, hx, y, hy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (hypothesis)
Goal:
𝕜_1 : Type u_4
E_1 : Type u_5
inst : Semiring 𝕜_1
inst_1 : PartialOrder 𝕜_1
inst_2 : AddCommMonoid E_1
inst_3 : SMul 𝕜_1 E_1
β_1 : Type u_6
γ_1 : Type u_7
inst_4 : LinearOrder β_1
inst_5 : Preorder γ_1
s_1 : Set E_1
f_1 : E_1 → β_1
g_1 : β_1 → γ_1
𝕜 : Type u_4
E : Type u_5
inst_6 : Semiring 𝕜
inst_7 : PartialOrder 𝕜
inst_8 : AddCommMonoid E
inst_9 : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst_10 : LinearOrder β
inst_11 : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
have hf₁ : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ f y} (a • x + b • y)
Tactic: specialize hf (f y) ⟨hx.1, h⟩ ⟨hy.1, le_rfl⟩ ha hb hab
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
β : Type u_6
inst_4 : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex.{u_4, u_5} 𝕜 (E := E) {x : E | x ∈ t ∧ f x ≤ b}
have rw : Convex 𝕜 (t ∩ {x : E | x ∈ s ∧ f x ≤ b})
Tactic: rw [Set.sep_eq_inter_sep hst]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
β : Type u_6
inst_4 : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex.{u_4, u_5} 𝕜 (E := E) {x : E | x ∈ t ∧ b ≤ f x}
have rw : Convex 𝕜 (t ∩ {x : E | x ∈ s ∧ b ≤ f x})
Tactic: rw [Set.sep_eq_inter_sep hst]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
E : Type u_4
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
β : Type u_5
inst_5 : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (α := (↑s : Type u_4)) (s ↓∩ f ⁻¹' Ici t)
have rw : IsPreconnected (s ∩ f ⁻¹' Ici t)
Tactic: rw [← Topology.IsInducing.subtypeVal.isPreconnected_image,
    image_preimage_eq_inter_range,
    Subtype.range_coe, inter_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
f g : E → β
inst_4 : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ (f ⊔ g) x ≤ r}
have simp_rw : Convex.{u_1, u_2} 𝕜 (E := E) ({x : E | x ∈ s ∧ f x ≤ r} ∩ {x : E | x ∈ s ∧ g x ≤ r})
Tactic: simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ QuasilinearOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
have rw : (Convex 𝕜 s ∧
    (∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
  Convex 𝕜 s ∧
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
Tactic: rw [QuasilinearOn, quasiconvexOn_iff_le_max, quasiconcaveOn_iff_min_le, and_and_and_comm,
    and_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      (∀ ⦃x : E⦄,
          x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
        ∀ ⦃x : E⦄,
          x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
have h : ((∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
    ∀ ⦃x : E⦄,
      x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
  ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
Tactic: apply and_congr_right'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
have h : (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5) (x_8 : x_4 + x_5 = 1),
    f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
  ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
Tactic: simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
h :
  (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5)
      (x_8 : x_4 + x_5 = 1),
      f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
have h₁ : (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5) (x_8 : x_4 + x_5 = 1),
    f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ Icc (min (f x) (f y)) (max (f x) (f y))
Tactic: simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
h :
  (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5)
      (x_8 : x_4 + x_5 = 1),
      f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
h₁ :
  (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5)
      (x_8 : x_4 + x_5 = 1),
      f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
    ∀ ⦃x : E⦄,
      x ∈ s →
        ∀ ⦃y : E⦄,
          y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ Icc (min (f x) (f y)) (max (f x) (f y))
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
have h₂ : (∀ (x : E) (x_1 : x ∈ s) (x_2 : E) (x_3 : x_2 ∈ s) (x_4 x_5 : 𝕜) (x_6 : 0 ≤ x_4) (x_7 : 0 ≤ x_5) (x_8 : x_4 + x_5 = 1),
    f (x_4 • x + x_5 • x_2) ≤ max (f x) (f x_2) ∧ min (f x) (f x_2) ≤ f (x_4 • x + x_5 • x_2)) ↔
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y) ∧ f (a • x + b • y) ≤ max (f x) (f y)
Tactic: simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} x) (y : E)
  (hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} y) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
  Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} (a • x + b • y)
Tactic: refine fun x hx y hy a b ha hb hab => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} (a • x + b • y)
have h : Membership.mem (γ := Set E) {x_1 : E | x_1 ∈ s ∧ f x_1 ≤ max (f x) (f y)} (a • x + b • y)
Tactic: have h := hf _ ⟨hx.1, le_max_left _ _⟩ ⟨hy.1, le_max_right _ _⟩ ha hb hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ MonotoneOn f s ∨ AntitoneOn f s
have simp_rw : ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
Tactic: simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
h_1 : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)
have refine_1 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} a
Tactic: refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
h_1 : c ∈ s
h : c ∈ segment 𝕜 a b
refine_1 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} a
⊢ f c ∈ uIcc (f a) (f b)
have refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} b
Tactic: refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩