awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → β
hf : QuasiconvexOn 𝕜 s f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}

Tactic:
fun x hx y hy a b ha hb hab => ?_

Premises used: Convex, 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 : LinearOrder β
inst_4 : SMul 𝕜 E
s : Set E
f : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
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)
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ f x < r}

Tactic:
refine fun x hx y hy a b ha hb hab => ?_
-- 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 → β
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_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
-- 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 → β
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
h : Membership.mem (γ := Set E) {x_1 : E | x_1 ∈ s ∧ f x_1 ≤ max (f x) (f y)} (a • x + b • y)
⊢ Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} (a • x + b • y)

Tactic:
⟨h.1, h.2.trans_lt <| max_lt hx.2 hy.2⟩

Premises used: Set.Mem, setOf, max_lt, And.right, And.left, And.intro, LE.le.trans_lt
-- 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 → β
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
h : Membership.mem (γ := Set E) {x_1 : E | x_1 ∈ s ∧ f x_1 ≤ max (f x) (f y)} (a • x + b • y)
⊢ Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x < r} (a • x + b • y)

Tactic:
exact ⟨h.1, h.2.trans_lt <| max_lt hx.2 hy.2⟩
-- 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 → β
hf : QuasiconcaveOn 𝕜 s f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ r < f x}

Tactic:
hf.dual.convex_lt r

Premises used: QuasiconvexOn.convex_lt, setOf, QuasiconcaveOn.dual
-- 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s f

Tactic:
hf.convex_le

Premises used: ConvexOn.convex_le, 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 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConcaveOn 𝕜 s f
⊢ QuasiconcaveOn 𝕜 s f

Tactic:
hf.convex_ge

Premises used: ConcaveOn.convex_ge, QuasiconcaveOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
⊢ QuasiconvexOn 𝕜 s f

Tactic:
hf.convex_le hs

Premises used: MonotoneOn.convex_le, 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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
⊢ QuasiconcaveOn 𝕜 s f

Tactic:
hf.convex_ge hs

Premises used: MonotoneOn.convex_ge, QuasiconcaveOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : MonotoneOn f s
hs : Convex 𝕜 s
⊢ QuasilinearOn 𝕜 s f

Tactic:
⟨hf.quasiconvexOn hs, hf.quasiconcaveOn hs⟩

Premises used: MonotoneOn.quasiconvexOn, QuasilinearOn, And.intro, MonotoneOn.quasiconcaveOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
⊢ QuasiconvexOn 𝕜 s f

Tactic:
hf.convex_le hs

Premises used: AntitoneOn.convex_le, 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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
⊢ QuasiconcaveOn 𝕜 s f

Tactic:
hf.convex_ge hs

Premises used: AntitoneOn.convex_ge, QuasiconcaveOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
⊢ QuasilinearOn 𝕜 s f

Tactic:
⟨hf.quasiconvexOn hs, hf.quasiconcaveOn hs⟩

Premises used: QuasilinearOn, AntitoneOn.quasiconcaveOn, And.intro, AntitoneOn.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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Monotone f
⊢ QuasiconvexOn 𝕜 univ f

Tactic:
(hf.monotoneOn _).quasiconvexOn convex_univ

Premises used: MonotoneOn.quasiconvexOn, convex_univ, Monotone.monotoneOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Monotone f
⊢ QuasiconcaveOn 𝕜 univ f

Tactic:
(hf.monotoneOn _).quasiconcaveOn convex_univ

Premises used: convex_univ, MonotoneOn.quasiconcaveOn, Monotone.monotoneOn
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Monotone f
⊢ QuasilinearOn 𝕜 univ f

Tactic:
⟨hf.quasiconvexOn, hf.quasiconcaveOn⟩

Premises used: Monotone.quasiconcaveOn, QuasilinearOn, And.intro, Monotone.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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
⊢ QuasiconvexOn 𝕜 univ f

Tactic:
(hf.antitoneOn _).quasiconvexOn convex_univ

Premises used: Antitone.antitoneOn, convex_univ, AntitoneOn.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 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
⊢ QuasiconcaveOn 𝕜 univ f

Tactic:
(hf.antitoneOn _).quasiconcaveOn convex_univ

Premises used: Antitone.antitoneOn, AntitoneOn.quasiconcaveOn, convex_univ
-- 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 E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
⊢ QuasilinearOn 𝕜 univ f

Tactic:
⟨hf.quasiconvexOn, hf.quasiconcaveOn⟩

Premises used: Antitone.quasiconvexOn, QuasilinearOn, And.intro, Antitone.quasiconcaveOn
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
simp_rw : ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
⊢ MonotoneOn f s ∨ AntitoneOn f s

Tactic:
simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]

Premises used: segment_eq_uIcc, Set.monotoneOn_or_antitoneOn_iff_uIcc
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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)

Tactic:
⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro, Set.uIcc, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} b
refine_3 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} a
refine_4 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} b
⊢ f c ∈ uIcc (f a) (f b)

Tactic:
refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} a

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} b

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} a

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Quasiconvex
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
⊢ Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} b

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Convex.Quasiconvex
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hs : Convex 𝕜 s
⊢ QuasilinearOn 𝕜 s f ↔ MonotoneOn f s ∨ AntitoneOn f s

Tactic:
⟨fun h => h.monotoneOn_or_antitoneOn, fun h =>
    h.elim (fun h => h.quasilinearOn hs) fun h => h.quasilinearOn hs⟩

Premises used: MonotoneOn.quasilinearOn, AntitoneOn.quasilinearOn, QuasilinearOn.monotoneOn_or_antitoneOn, Iff.intro, Or.elim
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ¬AffineIndependent 𝕜 f
⊢ ¬∀ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 → Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 → ∀ e ∈ s, w e = 0

Tactic:
rw [affineIndependent_iff] at h

Premises used: affineIndependent_iff
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ¬∀ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 → Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 → ∀ e ∈ s, w e = 0
⊢ ∃ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 ∧ Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 ∧ ∃ e ∈ s, w e ≠ 0

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ∃ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 ∧ Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 ∧ ∃ e ∈ s, w e ≠ 0
obtain :
  ∀ (s : Finset ι) (w : ι → 𝕜) (h_wsum : s.sum w = 0) (h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0)
    (nonzero_w_index : ι) (h1 : nonzero_w_index ∈ s) (h2 : w nonzero_w_index ≠ 0),
    ∃ (I : Set ι),
      Set.Nonempty.{u_3} (α := E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))

Tactic:
obtain ⟨s, w, h_wsum, h_vsum, nonzero_w_index, h1, h2⟩ := h
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
⊢ HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0

Tactic:
simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w

Premises used: not_lt, Finset.sum_filter_add_sum_filter_not, LT.lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
⊢ HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0

Tactic:
have hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0 := by
    simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
rcases : ∀ (pos_w_index : ι) (h1' : pos_w_index ∈ s) (h2' : 0 < w pos_w_index), LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
⊢ LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)

Tactic:
rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
      with ⟨pos_w_index, h1', h2'⟩

Premises used: And.intro, Exists.intro, Finset.exists_pos_of_sum_zero_of_exists_nonzero
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
pos_w_index : ι
h1' : pos_w_index ∈ s
h2' : 0 < w pos_w_index
⊢ pos_w_index ∈ I ∧ 0 < w pos_w_index

Tactic:
simp only [I, mem_filter, h1', h2'.le, and_self, h2']

Premises used: and_self, LT.lt.le, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
pos_w_index : ι
h1' : pos_w_index ∈ s
h2' : 0 < w pos_w_index
⊢ LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)

Tactic:
exact sum_pos' (fun _i hi ↦ (mem_filter.1 hi).2)
      ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩

Premises used: Finset.sum_pos', And.right, Exists.intro, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
⊢ LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)

Tactic:
have hI : 0 < ∑ i ∈ I, w i := by
    rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
      with ⟨pos_w_index, h1', h2'⟩
    exact sum_pos' (fun _i hi ↦ (mem_filter.1 hi).2)
      ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
⊢ HAdd.hAdd (α := E) (∑ i ∈ J, w i • f i) (∑ i ∈ I, w i • f i) = 0

Tactic:
simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _

Premises used: not_lt, Finset.sum_filter_add_sum_filter_not, LT.lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
⊢ J.centerMass w f = p

Tactic:
have hp : centerMass J w f = p := centerMass_of_sum_add_sum_eq_zero hJI <| by
    simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))

Tactic:
⟨I, p, ?_, ?_⟩

Premises used: SetLike.coe, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
refine_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)) : Set E) p
refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) p
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))

Tactic:
refine ⟨I, p, ?_, ?_⟩