awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z
have match_scalars : a₂ * a₁ * 1 = a₂ * (a₁ * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
⊢ (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z
have match_scalars₁ : (a₂ * b₁ + b₂) * (a₂ * b₁ / (a₂ * b₁ + b₂) * 1) = a₂ * (b₁ * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
⊢ (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z
have match_scalars₂ : (a₂ * b₁ + b₂) * (b₂ / (a₂ * b₁ + b₂) * 1) = b₂ * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
have refine : convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
Tactic: refine (convexJoin_assoc_aux _ _ _).antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
have simp_rw : convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
Tactic: simp_rw [convexJoin_comm s, convexJoin_comm _ u]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
have simp_rw : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 t s) u
Tactic: simp_rw [← convexJoin_assoc, convexJoin_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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 𝕜 (convexJoin 𝕜 s u) t
have simp_rw : convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 s (convexJoin 𝕜 u t)
Tactic: simp_rw [convexJoin_assoc, convexJoin_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
have simp_rw : convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s t) u) v = convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s u) t) v
Tactic: simp_rw [← convexJoin_assoc, convexJoin_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ Convex 𝕜 (convexJoin 𝕜 s t)
have 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]
Tactic: simp only [Convex, StarConvex, convexJoin, mem_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
have 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]
Tactic: rcases hs.exists_mem_add_smul_eq hx₁ hx₂ (mul_nonneg hp ha₁) (mul_nonneg hq ha₂) with ⟨x, hxs, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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₂
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
have 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]
Tactic: rcases ht.exists_mem_add_smul_eq hy₁ hy₂ (mul_nonneg hp hb₁) (mul_nonneg hq hb₂) with ⟨y, hyt, hy⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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]
have refine_1 : 0 ≤ p * a₁ + q * a₂
Tactic: refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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₂
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
have refine_2 : 0 ≤ p * b₁ + q * b₂
Tactic: refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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₂
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
have refine_3 : p * a₁ + q * a₂ + (p * b₁ + q * b₂) = 1
Tactic: refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ ∃ (i : E) (_ : i ∈ s) (i_1 : E) (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i -[𝕜] i_1]
have refine_4 : (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
Tactic: refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
have refine_4 : (p * a₁) • x₁ + (q * a₂) • x₂ + ((p * b₁) • y₁ + (q * b₂) • y₂) = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
Tactic: rw [hx, hy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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) (s ∪ t) : Set E)
    (convexJoin 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s) ((convexHull 𝕜 : (a : Set E) → Set E) t) : Set E)
have 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)
Tactic: rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ 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)
have 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)
Tactic: rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
⊢ 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)
have 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))
Tactic: rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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))
⊢ 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)
have rw₂ : Eq (α := Set E) (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s))
  (convexJoin 𝕜 {x} ((convexHull 𝕜 : (a : Set E) → Set E) s))
Tactic: rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d}
have 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})
Tactic: simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
    convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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})
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d}
have 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})))
Tactic: simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
    convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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})))
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d}
have 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}))))
Tactic: simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
    convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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}))))
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, d}
have 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}))))
Tactic: simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
    convexHull_insert (singleton_nonempty _), convexJoin_assoc,
    convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have rw : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c, c}
Tactic: rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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}
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have rw₁ : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c c)
Tactic: rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have rw₂ : convexJoin 𝕜 (segment 𝕜 a b) {c, c} = convexJoin 𝕜 (segment 𝕜 a b) {c}
Tactic: rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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}
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have rw₃ : convexJoin 𝕜 (segment 𝕜 a b) {c} = convexJoin 𝕜 (segment 𝕜 a b) {c}
Tactic: rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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
⊢ convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have rw : convexJoin 𝕜 (segment 𝕜 a a) (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
Tactic: rw [← segment_same 𝕜, convexJoin_segments, insert_idem]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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}
⊢ convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have 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)
Tactic: rw [← segment_same 𝕜, convexJoin_segments, insert_idem]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
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)
⊢ convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜 : (a : Set E) → Set E) {a, b, c}
have 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)
Tactic: rw [← segment_same 𝕜, convexJoin_segments, insert_idem]
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
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}
⊢ (extremePoints ℝ s).Nonempty
have rsuffices : ∀ (t : Set E) (ht : Minimal (fun (x : Set E) ↦ x ∈ S) t), (extremePoints ℝ s).Nonempty
Tactic: rsuffices ⟨t, ht⟩ : ∃ t, Minimal (· ∈ S) t