-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
refine :
  Subset (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
    ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ⊓ (↑t₂ : Set E)) : Set E)
refine₁ :
  ∀ (x : E),
    ((∃ (w : E → R), (∀ y ∈ t₁, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w y) 1 ∧ ∑ y ∈ t₁, w y • y = x) ∧
        ∃ (w : E → R), (∀ y ∈ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w y) 1 ∧ ∑ y ∈ t₂, w y • y = x) →
      ∃ (w : E → R),
        (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine₂ :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine₃ :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine₄ :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
    ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0),
      ∃ (w : E → R),
        (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine₅ :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
    ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0) (hs : ∀ x ∈ s, w x = 0),
      ∃ (w : E → R),
        (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine₆ :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
    ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0) (hs : ∀ x ∈ s, w x = 0)
      (ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0),
      ∃ (w : E → R),
        (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
refine_1 :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
    ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0) (hs : ∀ x ∈ s, w x = 0)
      (ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0), ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
refine_2 :
  ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
    (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
    (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
    let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
    ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0) (hs : ∀ x ∈ s, w x = 0)
      (ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0), Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ∩ (↑t₂ : Set E)) : Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
have refine_3 : ∀ (x : E) (w₁ : E → R) (h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y) (h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1)
  (h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x) (w₂ : E → R) (h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1)
  (h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x),
  let w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0;
  ∀ (h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0) (hs : ∀ x ∈ s, w x = 0)
    (ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0), ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x
Tactic: classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
    simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]
Cleared hypotheses: hs