𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
⊢ False
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∨
    ∃ u, u ∈ K.faces ∧ ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t = ↑(convexHull 𝕜).toOrderHom ↑u
by_contra' h
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
hst : s ∩ t = ∅
⊢ ↑(convexHull 𝕜).toOrderHom (↑s ∩ ↑t) ⊆ ⊥

case refine'_2
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
⊢ ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t = ↑(convexHull 𝕜).toOrderHom ↑(s ∩ t)
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
⊢ False
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 _) _
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
hst : s ∩ t = ∅
⊢ ↑(convexHull 𝕜).toOrderHom (↑s ∩ ↑t) ⊆ ⊥
rw [← coe_inter, hst, coe_empty, convexHull_empty]
no goals
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥
rfl
no goals
case refine'_2
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.25492
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (↑(convexHull 𝕜).toOrderHom ↑s) (↑(convexHull 𝕜).toOrderHom ↑t) ∧
    ∀ (u : Finset E),
      u ∈ K.faces → ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t ≠ ↑(convexHull 𝕜).toOrderHom ↑u
⊢ ↑(convexHull 𝕜).toOrderHom ↑s ∩ ↑(convexHull 𝕜).toOrderHom ↑t = ↑(convexHull 𝕜).toOrderHom ↑(s ∩ t)
rw [coe_inter, convexHull_inter_convexHull hs ht]