[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ↑(convexHull 𝕜) ↑s ⊆ space K
[PROOFSTEP]
convert subset_biUnion_of_mem hs
[GOAL]
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ↑(convexHull 𝕜) ↑s = ↑(convexHull 𝕜) ↑s
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∨
    ∃ u, u ∈ K.faces ∧ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑u
[PROOFSTEP]
classical
by_contra' h
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 _)
    _
· rw [← coe_inter, hst, coe_empty, convexHull_empty]
  rfl
· rw [coe_inter, convexHull_inter_convexHull hs ht]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∨
    ∃ u, u ∈ K.faces ∧ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑u
[PROOFSTEP]
by_contra' h
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
⊢ False
[PROOFSTEP]
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 _)
    _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ↑(convexHull 𝕜) (↑s ∩ ↑t) ⊆ ⊥
[PROOFSTEP]
rw [← coe_inter, hst, coe_empty, convexHull_empty]
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
hst : s ∩ t = ∅
⊢ ∅ ⊆ ⊥
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) ↑s) (↑(convexHull 𝕜) ↑t) ∧
    ∀ (u : Finset E), u ∈ K.faces → ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t ≠ ↑(convexHull 𝕜) ↑u
⊢ ↑(convexHull 𝕜) ↑s ∩ ↑(convexHull 𝕜) ↑t = ↑(convexHull 𝕜) ↑(s ∩ t)
[PROOFSTEP]
rw [coe_inter, convexHull_inter_convexHull hs ht]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
⊢ vertices K = ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈ vertices K ↔ x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
[PROOFSTEP]
refine' ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => _⟩
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
⊢ x ∈ vertices K
[PROOFSTEP]
obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h
[GOAL]
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
x✝ x : E
h : x ∈ ⋃ (k : Finset E) (_ : k ∈ K.faces), ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ vertices K
[PROOFSTEP]
exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_ne_empty _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
⊢ x ∈ ↑(convexHull 𝕜) ↑s ↔ x ∈ s
[PROOFSTEP]
refine' ⟨fun h => _, fun h => subset_convexHull 𝕜 _ h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ s
[PROOFSTEP]
classical
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
by_contra H
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm, coe_empty,
  convexHull_empty] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ s
[PROOFSTEP]
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜) ↑s
⊢ x ∈ ↑(convexHull 𝕜) ↑{x}
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜) ↑s
h : x ∈ ↑(convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s
[PROOFSTEP]
by_contra H
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜) ↑s
h : x ∈ ↑(convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
[PROOFSTEP]
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm, coe_empty,
  convexHull_empty] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ¬s ∈ facets K ↔ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
refine' ⟨fun hs' : ¬(_ ∧ _) => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
push_neg at hs' 
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
obtain ⟨t, ht⟩ := hs' hs
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
[PROOFSTEP]
exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ (∃ t, t ∈ K.faces ∧ s ⊂ t) → ¬s ∈ facets K
[PROOFSTEP]
rintro ⟨t, ht⟩ ⟨hs, hs'⟩
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ False
[PROOFSTEP]
have := hs' ht.1 ht.2.1
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
[PROOFSTEP]
rw [this] at ht 
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
[PROOFSTEP]
exact ht.2.2 (Subset.refl t)
