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 : 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:
exact 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
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ QuasiconvexOn 𝕜 s f → QuasiconcaveOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
id

Premises used: setOf, id, QuasiconcaveOn, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
id

Premises used: setOf, id, OrderDual, QuasiconvexOn
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
⊢ QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 (β := βᵒᵈ) s ((⇑toDual : (a : β) → βᵒᵈ) ∘ f)

Tactic:
And.symm

Premises used: QuasilinearOn, setOf, QuasiconcaveOn, OrderDual, And.symm, QuasiconvexOn
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
hs : Convex 𝕜 s
h : ∀ (r : β), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x ≤ r}
⊢ QuasiconvexOn 𝕜 s f

Tactic:
fun r => hs.inter (h r)

Premises used: Set.Mem, setOf, Set.inter, Convex.inter, QuasiconvexOn
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
hs : Convex 𝕜 s
h : ∀ (r : β), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | r ≤ f x}
⊢ QuasiconcaveOn 𝕜 s f

Tactic:
Convex.quasiconvexOn_of_convex_le (β := βᵒᵈ) hs h

Premises used: Convex.quasiconvexOn_of_convex_le, setOf, QuasiconcaveOn, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
inst_5 : IsDirectedOrder β
hf : QuasiconvexOn 𝕜 s f
⊢ Convex 𝕜 s

Tactic:
fun x hx y hy _ _ ha hb hab =>
  let ⟨_, hxz, hyz⟩ := exists_ge_ge (f x) (f y)
  (hf _ ⟨hx, hxz⟩ ⟨hy, hyz⟩ ha hb hab).1

Premises used: Membership.mem, exists_ge_ge, And.left, HAdd.hAdd, Convex, And.intro, HSMul.hSMul, _private.0.QuasiconvexOn.convex.match_1, StarConvex
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LE β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
inst_5 : IsCodirectedOrder β
hf : QuasiconcaveOn 𝕜 s f
⊢ Convex 𝕜 s

Tactic:
hf.dual.convex

Premises used: QuasiconvexOn.convex, QuasiconcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
simp : a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
⊢ Membership.mem (γ := Set E) {x : E | x ∈ s ∧ (g ∘ f) x ≤ c} (a • x + b • y)

Tactic:
simp only [Function.comp_apply, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Function.comp_apply
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
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
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

Tactic:
wlog h : f x ≤ f y
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
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:
grind
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
⊢ 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

Premises used: le_rfl, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
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
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

Tactic:
⟨hf.1, le_trans (hg hf.2) hy.2⟩

Premises used: And.right, And.left, And.intro, le_trans
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
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
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

Tactic:
exact ⟨hf.1, le_trans (hg hf.2) hy.2⟩
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : Antitone g
hf : QuasiconvexOn 𝕜 s f
⊢ QuasiconcaveOn 𝕜 s (g ∘ f)

Tactic:
hf.monotone_comp (γ := γᵒᵈ) hg

Premises used: setOf, QuasiconvexOn.monotone_comp, QuasiconcaveOn, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : QuasiconcaveOn 𝕜 s f
⊢ QuasiconcaveOn 𝕜 s (g ∘ f)

Tactic:
QuasiconvexOn.monotone_comp hg.dual hf

Premises used: setOf, Monotone.dual, QuasiconvexOn.monotone_comp, QuasiconcaveOn, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : Antitone g
hf : QuasiconcaveOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s (g ∘ f)

Tactic:
QuasiconvexOn.monotone_comp (β := βᵒᵈ) hg.dual hf

Premises used: Antitone.dual, QuasiconvexOn.monotone_comp
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : QuasilinearOn 𝕜 s f
⊢ QuasilinearOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.1.monotone_comp hg, hf.2.monotone_comp hg⟩

Premises used: QuasiconcaveOn.monotone_comp, QuasilinearOn, QuasiconvexOn.monotone_comp, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : Antitone g
hf : QuasilinearOn 𝕜 s f
⊢ QuasilinearOn 𝕜 s (g ∘ f)

Tactic:
⟨hf.2.antitone_comp hg, hf.1.antitone_comp hg⟩

Premises used: QuasiconcaveOn.antitone_comp, QuasilinearOn, QuasiconvexOn.antitone_comp, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : β
rw : Convex 𝕜 (t ∩ {x : E | x ∈ s ∧ f x ≤ b})
⊢ Convex.{u_4, u_5} 𝕜 (E := E) {x : E | x ∈ t ∧ f x ≤ b}

Tactic:
rw [Set.sep_eq_inter_sep hst]

Premises used: Set.sep_eq_inter_sep
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 𝕜 (t ∩ {x : E | x ∈ s ∧ f x ≤ b})

Tactic:
Convex.inter ht (hf b)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 𝕜 (t ∩ {x : E | x ∈ s ∧ f x ≤ b})

Tactic:
exact Convex.inter ht (hf b)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : β
rw : Convex 𝕜 (t ∩ {x : E | x ∈ s ∧ b ≤ f x})
⊢ Convex.{u_4, u_5} 𝕜 (E := E) {x : E | x ∈ t ∧ b ≤ f x}

Tactic:
rw [Set.sep_eq_inter_sep hst]

Premises used: Set.sep_eq_inter_sep
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 𝕜 (t ∩ {x : E | x ∈ s ∧ b ≤ f x})

Tactic:
Convex.inter ht (hf b)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 𝕜 (t ∩ {x : E | x ∈ s ∧ b ≤ f x})

Tactic:
exact Convex.inter ht (hf b)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
rw : IsPreconnected (s ∩ f ⁻¹' Ici t)
⊢ IsPreconnected (α := (↑s : Type u_4)) (s ↓∩ f ⁻¹' Ici t)

Tactic:
rw [← Topology.IsInducing.subtypeVal.isPreconnected_image,
    image_preimage_eq_inter_range,
    Subtype.range_coe, inter_comm]

Premises used: Topology.IsInducing.isPreconnected_image, Subtype.range_coe, Set.image_preimage_eq_inter_range, Set.inter_comm, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 ∩ f ⁻¹' Ici t)

Tactic:
(hfc t).isPreconnected

Premises used: Set.Ici, Set.Mem, setOf, Set.inter, Set.preimage, Convex.isPreconnected
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 ∩ f ⁻¹' Ici t)

Tactic:
exact (hfc t).isPreconnected

Premises used: Convex.isPreconnected
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : QuasiconvexOn ℝ s f
⊢ IsPreconnected (α := (↑s : Type u_4)) (s ↓∩ f ⁻¹' Iic t)

Tactic:
QuasiconcaveOn.isPreconnected_preimage_subtype (β := βᵒᵈ) hfc

Premises used: setOf, QuasiconcaveOn.isPreconnected_preimage_subtype, Set.Iic, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : QuasilinearOn ℝ s f
⊢ IsPreconnected (α := (↑s : Type u_4)) (s ↓∩ f ⁻¹' Iic t)

Tactic:
hfc.left.isPreconnected_preimage_subtype

Premises used: QuasiconvexOn.isPreconnected_preimage_subtype, And.left
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : β
simp_rw : Convex.{u_1, u_2} 𝕜 (E := E) ({x : E | x ∈ s ∧ f x ≤ r} ∩ {x : E | x ∈ s ∧ g x ≤ r})
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ (f ⊔ g) x ≤ r}

Tactic:
simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]

Premises used: sup_le_iff, Pi.sup_def, Set.sep_and
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 x ≤ r} ∩ {x : E | x ∈ s ∧ g x ≤ r})

Tactic:
(hf r).inter (hg r)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 x ≤ r} ∩ {x : E | x ∈ s ∧ g x ≤ r})

Tactic:
exact (hf r).inter (hg r)

Premises used: Convex.inter
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 : SemilatticeInf β
hf : QuasiconcaveOn 𝕜 s f
hg : QuasiconcaveOn 𝕜 s g
⊢ QuasiconcaveOn 𝕜 s (f ⊓ g)

Tactic:
hf.dual.sup hg

Premises used: setOf, QuasiconvexOn.sup, QuasiconcaveOn, QuasiconcaveOn.dual, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 → β
⊢ QuasiconvexOn 𝕜 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) ≤ max (f x) (f y)

Tactic:
⟨fun hf =>
    ⟨hf.convex, fun _ hx _ hy _ _ ha hb hab =>
      (hf _ ⟨hx, le_max_left _ _⟩ ⟨hy, le_max_right _ _⟩ ha hb hab).2⟩,
    fun hf _ _ hx _ hy _ _ ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha hb hab, (hf.2 hx.1 hy.1 ha hb hab).trans <| max_le hx.2 hy.2⟩⟩

Premises used: le_max_right, And.right, And.left, Max.max, QuasiconvexOn.convex, And.intro, max_le, Iff.intro, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 → β
⊢ QuasiconcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃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)

Tactic:
quasiconvexOn_iff_le_max (β := βᵒᵈ)

Premises used: setOf, quasiconvexOn_iff_le_max, QuasiconcaveOn, OrderDual
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 → β
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)
⊢ 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)

Tactic:
rw [QuasilinearOn, quasiconvexOn_iff_le_max, quasiconcaveOn_iff_min_le, and_and_and_comm,
    and_self_iff]

Premises used: quasiconcaveOn_iff_min_le, QuasilinearOn, quasiconvexOn_iff_le_max, and_and_and_comm, and_self_iff
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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 ∈ 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)
⊢ (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:
apply and_congr_right'

Premises used: and_congr_right'
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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))
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)
⊢ ((∀ ⦃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:
simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]

Premises used: Set.Icc_min_max, and_comm, Set.mem_Icc, forall_and