-- Lean 4 proof step from Mathlib.Analysis.Convex.SimplicialComplex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ :
  ¬(Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
        ∃ u ∈ K.faces,
          Eq (α := Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
              Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)) →
    False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ :
  ∀
    (h :
      ¬Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∧
        ∀ (u : Finset E) (_ : u ∈ K.faces),
          Ne (α := Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
              Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
    False
by_contra!₁₁ :
  ∀
    (h :
      Set.Nonempty.{u_2} (α := E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
        ∀ (u : Finset E) (_ : u ∈ K.faces),
          Ne (α := Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
              Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
    False
refine_1 :
  ∀
    (h :
      Set.Nonempty.{u_2} (α := E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
        ∀ (u : Finset E) (_ : u ∈ K.faces),
          Ne (α := Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
              Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
    (s ∩ t).Nonempty
⊢ Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
    ∃ u ∈ K.faces,
      Eq (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
have refine_2 : ∀
  (h :
    Set.Nonempty.{u_2} (α := E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
      ∀ (u : Finset E) (_ : u ∈ K.faces),
        Ne (α := Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
            Set E)
          ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
  Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)
Tactic: classical
  by_contra! h
  rw [not_disjoint_iff_nonempty_inter] at h
  refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_
  · simpa [← coe_inter] using convexHull_nonempty_iff.1 (h.1.mono (K.inter_subset_convexHull hs ht))
  · rw [coe_inter, convexHull_inter_convexHull hs ht]