-- Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
theorem disjoint_or_exists_inter_eq_convexHull (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
    Disjoint (convexHull 𝕜 (s : Set E)) (convexHull 𝕜 ↑t) ∨
      ∃ u ∈ K.faces, convexHull 𝕜 (s : Set E) ∩ convexHull 𝕜 ↑t = convexHull 𝕜 ↑u

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨
    ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u

Tactic:
by_contra! h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ False

Tactic:
refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left fun hst => h.1 <|
  disjoint_iff_inf_le.mpr <| (K.inter_subset_convexHull hs ht).trans ?_) ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ (convexHull 𝕜) (↑s ∩ ↑t) ⊆ ⊥

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑(s ∩ t)

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑(s ∩ t)

Tactic:
rw [coe_inter, convexHull_inter_convexHull hs ht]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ (convexHull 𝕜) (↑s ∩ ↑t) ⊆ ⊥

Tactic:
rw [← coe_inter, hst, coe_empty, convexHull_empty]

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥