awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ * a₁ + (a₂ * b₁ + b₂) = 1

Tactic:
linear_combination a₂ * hab₁ + 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₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
match_scalars : a₂ * a₁ * 1 = a₂ * (a₁ * 1)
match_scalars₁ : (a₂ * b₁ + b₂) * (a₂ * b₁ / (a₂ * b₁ + b₂) * 1) = a₂ * (b₁ * 1)
match_scalars₂ : (a₂ * b₁ + b₂) * (b₂ / (a₂ * b₁ + b₂) * 1) = b₂ * 1
⊢ (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z

Tactic:
match_scalars
-- 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₂ * a₁ * 1 = a₂ * (a₁ * 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₂
⊢ (a₂ * b₁ + b₂) * (a₂ * b₁ / (a₂ * b₁ + b₂) * 1) = a₂ * (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₂
⊢ (a₂ * b₁ + b₂) * (b₂ / (a₂ * b₁ + b₂) * 1) = 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
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
(convexJoin_assoc_aux _ _ _).antisymm ?_

Premises used: HasSubset.Subset.antisymm, convexJoin_assoc_aux
-- 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
refine : convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
refine (convexJoin_assoc_aux _ _ _).antisymm ?_

Premises used: HasSubset.Subset.antisymm, convexJoin_assoc_aux
-- 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 : convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u

Tactic:
simp_rw [convexJoin_comm s, convexJoin_comm _ u]

Premises used: convexJoin_comm
-- 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
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)

Tactic:
convexJoin_assoc_aux _ _ _

Premises used: convexJoin_assoc_aux
-- 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
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)

Tactic:
exact convexJoin_assoc_aux _ _ _

Premises used: convexJoin_assoc_aux
-- 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 : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 t s) u
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

Tactic:
simp_rw [← convexJoin_assoc, convexJoin_comm]

Premises used: convexJoin_assoc, convexJoin_comm
-- 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 : convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 s (convexJoin 𝕜 u t)
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

Tactic:
simp_rw [convexJoin_assoc, convexJoin_comm]

Premises used: convexJoin_assoc, convexJoin_comm
-- 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 v : Set E
simp_rw : convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s t) u) v = convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s u) t) v
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Tactic:
simp_rw [← convexJoin_assoc, convexJoin_right_comm]

Premises used: convexJoin_assoc, convexJoin_right_comm
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
simp :
  ∀ ⦃x : E⦄,
    (∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), x ∈ [i -[𝕜] i_1]) →
      ∀ ⦃y : E⦄,
        (∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), y ∈ [i -[𝕜] i_1]) →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a → 0 ≤ b → a + b = 1 → ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), a • x + b • y ∈ [i -[𝕜] i_1]
⊢ Convex 𝕜 (convexJoin 𝕜 s t)

Tactic:
simp only [Convex, StarConvex, convexJoin, mem_iUnion]

Premises used: convexJoin, Set.mem_iUnion, Convex, StarConvex
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
rcases :
  ∀ (x : E) (hxs : x ∈ s) (hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂),
    ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]

Tactic:
rcases hs.exists_mem_add_smul_eq hx₁ hx₂ (mul_nonneg hp ha₁) (mul_nonneg hq ha₂) with ⟨x, hxs, hx⟩

Premises used: mul_nonneg, Convex.exists_mem_add_smul_eq
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
rcases :
  ∀ (y : E) (hyt : y ∈ t) (hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂),
    ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]

Tactic:
rcases ht.exists_mem_add_smul_eq hy₁ hy₂ (mul_nonneg hp hb₁) (mul_nonneg hq hb₂) with ⟨y, hyt, hy⟩

Premises used: mul_nonneg, Convex.exists_mem_add_smul_eq
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]

Tactic:
⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
refine_1 : 0 ≤ p * a₁ + q * a₂
refine_2 : 0 ≤ p * b₁ + q * b₂
refine_3 : p * a₁ + q * a₂ + (p * b₁ + q * b₂) = 1
refine_4 : (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]

Tactic:
refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * a₁ + q * 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * a₁ + q * a₂

Tactic:
try 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * b₁ + q * 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ 0 ≤ p * b₁ + q * b₂

Tactic:
try 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ p * a₁ + q * a₂ + (p * b₁ + q * b₂) = 1

Tactic:
linear_combination p * hab₁ + q * hab₂ + hpq
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
refine_4 :
  (p * a₁) • x₁ + (q * a₂) • x₂ + ((p * b₁) • y₁ + (q * b₂) • y₂) = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
⊢ (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)

Tactic:
rw [hx, hy]
-- 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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ (p * a₁) • x₁ + (q * a₂) • x₂ + ((p * b₁) • y₁ + (q * b₂) • y₂) = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)

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 : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hs₀ : s.Nonempty
ht₀ : t.Nonempty
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (s ∪ t) = convexJoin 𝕜 s t

Tactic:
(convexHull_min (union_subset (subset_convexJoin_left ht₀) <| subset_convexJoin_right hs₀) <|
        hs.convexJoin ht).antisymm <|
    convexJoin_subset_convexHull _ _

Premises used: convexJoin_subset_convexHull, Set.union_subset, subset_convexJoin_left, HasSubset.Subset.antisymm, subset_convexJoin_right, convexHull_min, Convex.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 : Set E
hs : s.Nonempty
ht : t.Nonempty
rw :
  Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) s ∪ (convexHull 𝕜 : (a : Set E) → Set E) t : Set E) :
      Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s) ((convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s ∪ t) : Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s) ((convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)

Tactic:
rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]

Premises used: convexHull_convexHull_union_right, convexHull_convexHull_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 : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) s ∪ (convexHull 𝕜 : (a : Set E) → Set E) t : Set E) :
      Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s) ((convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)

Tactic:
(convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull

Premises used: Convex.convexHull_union, convex_convexHull, Set.Nonempty.convexHull
-- 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 : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) s ∪ (convexHull 𝕜 : (a : Set E) → Set E) t : Set E) :
      Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s) ((convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)

Tactic:
exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull

Premises used: Convex.convexHull_union, convex_convexHull, Set.Nonempty.convexHull
-- 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 : Set E
x : E
hs : s.Nonempty
rw :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ({x} ∪ s) : Set E)
    (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set E)
rw₁ :
  Eq (α := Set E) (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) {x}) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s))
rw₂ rw₃ :
  Eq (α := Set E) (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s))
    (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s))
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (insert x s) : Set E)
    (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set E)

Tactic:
rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]

Premises used: Set.singleton_nonempty, Set.insert_eq, convexHull_singleton, convexHull_union
-- 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
a b c d : E
simp_rw :
  Eq.{u_3 + 1} (α := Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) {a, b}) ((convexHull 𝕜 : (a : Set E) → Set E) {c, d}))
    ((convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d})
simp_rw₁ :
  Eq (α := Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) {a, b}) ((convexHull 𝕜 : (a : Set E) → Set E) {c, d}))
    (convexJoin 𝕜 {a} (convexJoin 𝕜 {b} ((convexHull 𝕜 : (a : Set E) → Set E) {c, d})))
simp_rw₂ :
  Eq (α := Set E)
    (convexJoin 𝕜 (convexJoin 𝕜 {a} ((convexHull 𝕜 : (a : Set E) → Set E) {b}))
      (convexJoin 𝕜 {c} ((convexHull 𝕜 : (a : Set E) → Set E) {d})))
    (convexJoin 𝕜 {a} (convexJoin 𝕜 {b} (convexJoin 𝕜 {c} ((convexHull 𝕜 : (a : Set E) → Set E) {d}))))
simp_rw₃ :
  Eq (α := Set E)
    (convexJoin 𝕜 {a}
      (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) {b})
        (convexJoin 𝕜 {c} ((convexHull 𝕜 : (a : Set E) → Set E) {d}))))
    (convexJoin 𝕜 {a} (convexJoin 𝕜 {b} (convexJoin 𝕜 {c} ((convexHull 𝕜 : (a : Set E) → Set E) {d}))))
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d}

Tactic:
simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
    convexHull_singleton]

Premises used: Set.singleton_nonempty, convexHull_insert, Set.insert_nonempty, convexJoin_assoc, convexHull_pair, convexHull_singleton
-- 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
a b c : E
rw : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, c}
rw₁ : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c c)
rw₂ : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = convexJoin 𝕜 (segment 𝕜 a b) {c}
rw₃ rw₄ : convexJoin 𝕜 (segment 𝕜 a b) {c} = convexJoin 𝕜 (segment 𝕜 a b) {c}
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}

Tactic:
rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]

Premises used: convexJoin_segments, segment_same, Set.pair_eq_singleton
-- 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
a b c : E
rw : convexJoin 𝕜 (segment 𝕜 a a) (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
rw₁ :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {a, a, b, c} : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) {a, b, c} : Set E)
rw₂ rw₃ :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {a, b, c} : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) {a, b, c} : Set E)
⊢ convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}

Tactic:
rw [← segment_same 𝕜, convexJoin_segments, insert_idem]

Premises used: convexJoin_segments, segment_same, Set.insert_idem
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
rsuffices : ∀ (t : Set E) (ht : Minimal (fun (x : Set E) ↦ x ∈ S) t), (extremePoints ℝ s).Nonempty
rsuffices₁ : ∃ (t : Set E), Minimal (fun (x : Set E) ↦ x ∈ S) t
⊢ (extremePoints ℝ s).Nonempty

Tactic:
rsuffices ⟨t, ht⟩ : ∃ t, Minimal (· ∈ S) t
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t : Set E | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun (x : Set E) ↦ x ∈ S) t
obtain : ∀ (x : E) (hxt : x ∈ t) (htclos : IsClosed t) (hst : IsExtreme ℝ s t), (extremePoints ℝ s).Nonempty
⊢ (extremePoints ℝ s).Nonempty

Tactic:
obtain ⟨⟨x, hxt⟩, htclos, hst⟩ := ht.prop

Premises used: Minimal.prop