awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t_1 : Set E
hf : ConvexOn 𝕜 s f
hts : t_1 ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hp : ∀ i ∈ t, p i ∈ t_1
i : α
hit : i ∈ t
Hi : f (t.centerMass w p) ≤ f (p i)
⊢ ∃ y ∈ t_1, f (t.centerMass w p) ≤ f y

Tactic:
exact ⟨p i, hp i hit, Hi⟩
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConcaveOn 𝕜 s f
hts : t ⊆ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
⊢ ∃ y ∈ t, f y ≤ f x

Tactic:
hf.dual.exists_ge_of_mem_convexHull hts hx

Premises used: ConvexOn.exists_ge_of_mem_convexHull, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {x, y} : Set E) z

Tactic:
rw [← convexHull_pair] at hz

Premises used: convexHull_pair
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {x, y} : Set E) z
⊢ f z ≤ max (f x) (f y)

Tactic:
simpa using hf.exists_ge_of_mem_convexHull (pair_subset hx hy) hz

Premises used: Set.pair_subset, ConvexOn.exists_ge_of_mem_convexHull
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConcaveOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ min (f x) (f y) ≤ f z

Tactic:
hf.dual.le_max_of_mem_segment hx hy hz

Premises used: ConcaveOn.dual, ConvexOn.le_max_of_mem_segment
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ z ∈ [x -[𝕜] y]

Tactic:
rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz

Premises used: segment_eq_Icc, And.right, And.left, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)

Tactic:
hf.le_max_of_mem_segment hx hy hz

Premises used: ConvexOn.le_max_of_mem_segment
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)

Tactic:
exact hf.le_max_of_mem_segment hx hy hz

Premises used: ConvexOn.le_max_of_mem_segment
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConcaveOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ min (f x) (f y) ≤ f z

Tactic:
hf.dual.le_max_of_mem_Icc hx hy hz

Premises used: ConvexOn.le_max_of_mem_Icc, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ BddAbove (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
⟨b, ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
refine : b ∈ upperBounds (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)
⊢ BddAbove (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
refine ⟨b, ?_⟩
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
obtain : ∀ (y : E) (hy : y ∈ s) (hxy : f x ≤ f y), f x ≤ b
⊢ f x ≤ b

Tactic:
obtain ⟨y, hy, hxy⟩ := hf.exists_ge_of_mem_convexHull hst hx

Premises used: ConvexOn.exists_ge_of_mem_convexHull
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
y : E
hy : y ∈ s
hxy : f x ≤ f y
⊢ f x ≤ b

Tactic:
hxy.trans <| hb <| mem_image_of_mem _ hy

Premises used: Set.mem_image_of_mem, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
y : E
hy : y ∈ s
hxy : f x ≤ f y
⊢ f x ≤ b

Tactic:
exact hxy.trans <| hb <| mem_image_of_mem _ hy

Premises used: Set.mem_image_of_mem, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConcaveOn 𝕜 t f
⊢ BddBelow (f '' s) → BddBelow (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
hf.dual.bddAbove_convexHull hst

Premises used: lowerBounds, Set.Mem, setOf, ConvexOn.bddAbove_convexHull, BddBelow, OrderDual, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
x : E
⊢ x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b

Tactic:
simp [convexJoin]

Premises used: convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s₁ s₂ t₁ t₂ : Set E
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂

Tactic:
biUnion_mono hs fun _ _ => biUnion_subset_biUnion_left ht

Premises used: convexJoin, Set.biUnion_mono, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t s₁ s₂ : Set E
hs : s₁ ⊆ s₂
⊢ convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t

Tactic:
convexJoin_mono hs Subset.rfl

Premises used: convexJoin_mono, Set.Subset.rfl
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t₁ t₂ : Set E
ht : t₁ ⊆ t₂
⊢ convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂

Tactic:
convexJoin_mono Subset.rfl ht

Premises used: convexJoin_mono, Set.Subset.rfl
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t : Set E
⊢ convexJoin 𝕜 ∅ t = ∅

Tactic:
simp [convexJoin]

Premises used: convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ convexJoin 𝕜 s ∅ = ∅

Tactic:
simp [convexJoin]

Premises used: convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t : Set E
x : E
⊢ convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y

Tactic:
simp [convexJoin]

Premises used: convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
y : E
⊢ convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y

Tactic:
simp [convexJoin]

Premises used: convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
y x : E
⊢ convexJoin 𝕜 {x} {y} = segment 𝕜 x y

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s₁ s₂ t : Set E
simp_rw :
  Eq.{u_3 + 1} (α := Set E) (⋃ x ∈ s₁ ∪ s₂, ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
simp_rw₁ :
  Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (_ : x ∈ s₁ ∨ x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
simp_rw₂ :
  Eq.{u_3 + 1} (α := Set E)
    (⋃ (x : E), (⋃ (_ : x ∈ s₁), ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ (_ : x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

Tactic:
simp_rw [convexJoin, mem_union, iUnion_or, iUnion_union_distrib]

Premises used: Set.mem_union, convexJoin, Set.iUnion_union_distrib, Set.iUnion_or
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t₁ t₂ : Set E
simp_rw : convexJoin 𝕜 (t₁ ∪ t₂) s = convexJoin 𝕜 t₁ s ∪ convexJoin 𝕜 t₂ s
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

Tactic:
simp_rw [convexJoin_comm s, convexJoin_union_left]

Premises used: convexJoin_union_left, convexJoin_comm
-- Module: Mathlib.Analysis.Convex.Join
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : ι → Set E
t : Set E
simp_rw :
  Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (i : ι), ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y)
    (⋃ (i : ι), ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y)
⊢ convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t

Tactic:
simp_rw [convexJoin, mem_iUnion, iUnion_exists]

Premises used: convexJoin, Set.mem_iUnion, Set.iUnion_exists
-- Module: Mathlib.Analysis.Convex.Join
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (i : ι), ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y)
    (⋃ (i : ι), ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y)

Tactic:
iUnion_comm _

Premises used: Set.iUnion_comm
-- Module: Mathlib.Analysis.Convex.Join
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (i : ι), ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y)
    (⋃ (i : ι), ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y)

Tactic:
exact iUnion_comm _

Premises used: Set.iUnion_comm
-- Module: Mathlib.Analysis.Convex.Join
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
t : ι → Set E
simp_rw : convexJoin 𝕜 (⋃ (i : ι), t i) s = ⋃ (i : ι), convexJoin 𝕜 (t i) s
⊢ convexJoin 𝕜 s (⋃ (i : ι), t i) = ⋃ (i : ι), convexJoin 𝕜 s (t i)

Tactic:
simp_rw [convexJoin_comm s, convexJoin_iUnion_left]

Premises used: convexJoin_iUnion_left, convexJoin_comm
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
x y : E
hx : x ∈ s
hy : y ∈ t
⊢ segment 𝕜 x y ⊆ convexJoin 𝕜 s t

Tactic:
subset_iUnion₂_of_subset x hx <| subset_iUnion₂ (s := fun y _ ↦ segment 𝕜 x y) y hy

Premises used: Set.subset_iUnion₂, convexJoin, Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
inst_4 : IsOrderedRing 𝕜
h : t.Nonempty
⊢ s ⊆ convexJoin 𝕜 s t

Tactic:
fun _x hx =>
  let ⟨_y, hy⟩ := h
  segment_subset_convexJoin hx hy <| left_mem_segment _ _ _

Premises used: _private.0.subset_convexJoin_left.match_1, left_mem_segment, convexJoin, segment_subset_convexJoin, Membership.mem, Set.Subset
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
inst_4 : IsOrderedRing 𝕜
h : s.Nonempty
⊢ t ⊆ convexJoin 𝕜 s t

Tactic:
convexJoin_comm (𝕜 := 𝕜) t s ▸ subset_convexJoin_left h

Premises used: Eq.rec, subset_convexJoin_left, convexJoin_comm
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t u : Set E
hs : s ⊆ u
ht : t ⊆ u
hu : Convex 𝕜 u
⊢ convexJoin 𝕜 s t ⊆ u

Tactic:
iUnion₂_subset fun _x hx => iUnion₂_subset fun _y hy => hu.segment_subset (hs hx) (ht hy)

Premises used: Set.iUnion₂_subset, convexJoin, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t : Set E
⊢ convexJoin 𝕜 s t ⊆ (convexHull 𝕜 : (a : Set E) → Set E) (s ∪ t)

Tactic:
convexJoin_subset (subset_union_left.trans <| subset_convexHull _ _)
      (subset_union_right.trans <| subset_convexHull _ _) <|
    convex_convexHull _ _

Premises used: convexJoin_subset, subset_convexHull, Set.subset_union_right, HasSubset.Subset.trans, convex_convexHull, Set.subset_union_left
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
simp_rw :
  ∀ (x : E),
    (∃ (a : E), (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) →
      ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
simp_rw [subset_def, mem_convexJoin]

Premises used: Set.subset_def, mem_convexJoin
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
inl :
  ∀ (hb₂ : LE.le.{u_2} (α := 𝕜) 0 0) (hab₂ : a₂ + 0 = 1),
    ∃ a ∈ s,
      ∃ (b : E),
        (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
          a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b
inr :
  ∀ (hb₂ : 0 < b₂),
    ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b

Tactic:
obtain rfl | hb₂ := hb₂.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
⊢ ∃ a ∈ s,
    ∃ (b : E),
      (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
        a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b

Tactic:
⟨x, hx, y, ⟨y, hy, z, hz, left_mem_segment 𝕜 _ _⟩, a₁, b₁, ha₁, hb₁, hab₁, ?_⟩

Premises used: left_mem_segment, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
inl : a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z
⊢ ∃ a ∈ s,
    ∃ (b : E),
      (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
        a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b

Tactic:
refine ⟨x, hx, y, ⟨y, hy, z, hz, left_mem_segment 𝕜 _ _⟩, a₁, b₁, ha₁, hb₁, hab₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
⊢ a₁ • x + b₁ • y + (a₂ + 0) • (a₁ • x + b₁ • y) -
      (a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z +
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 1 (a₁ • x + b₁ • y)) =
    0

Tactic:
module
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
a :
  a₁ • x + b₁ • y + (a₂ + 0) • (a₁ • x + b₁ • y) -
      (a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z +
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 1 (a₁ • x + b₁ • y)) =
    0
⊢ a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z

Tactic:
linear_combination (norm := module) -hab₂ • (a₁ • x + b₁ • y)

Premises used: HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * b₁ / (a₂ * b₁ + b₂)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ b₂ / (a₂ * b₁ + b₂)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * b₁ / (a₂ * b₁ + b₂) + b₂ / (a₂ * b₁ + b₂) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * a₁

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * b₁ + b₂

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Join
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
inr : a₂ * a₁ + (a₂ * b₁ + b₂) = 1
inr₁ :
  (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b

Tactic:
refine
    ⟨x, hx, (a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z,
      ⟨y, hy, z, hz, _, _, by positivity, by positivity, by field, rfl⟩,
      a₂ * a₁, a₂ * b₁ + b₂, by positivity, by positivity, ?_, ?_⟩