Cone Subdivisions (Case 3 of Theorem 7.1)🔗

Given a simplicial complex and an apex point lying off the affine span of its underlying space, the cone over it is again a simplicial complex, whose underlying space is the convex join. This is the inductive step of Case 3 of Theorem 7.1. The verification, from the informal proof:

Affine independence: \{v\}\cup\sigma is affinely independent because \sigma is and v lies off the affine span of K's space (which contains \sigma).
Downward closure: a nonempty subset of \{v\}\cup\sigma either omits v (then it is a subset of \sigma, a face of K) or is \{v\}\cup\sigma' for a subset \sigma' \subseteq \sigma (a face of K if nonempty, else the face \{v\}).
Gluing: the key observation is uniqueness of the apex height: if (1-a)v + a\,b = (1-a')v + a'\,b' with b, b' in the affine span of P' and a \ne a', then one can solve for v as an affine combination of b and b', putting v in that span — contradiction; so a = a'. Given this, a point in the intersection of two cone cells \operatorname{conv}(\{v\}\cup\sigma) and \operatorname{conv}(\{v\}\cup\tau) has a common height a; if a = 0 the point is v; otherwise the base points agree and lie in \operatorname{conv}(\sigma)\cap\operatorname{conv}(\tau) \subseteq \operatorname{conv}(\sigma\cap\tau) (gluing in K), so the point lies in \operatorname{conv}(\{v\}\cup(\sigma\cap\tau)). The mixed cases (one cell coned, one not) are handled the same way: a point of \operatorname{conv}(\sigma) (\sigma a face of K) lies in the affine span of P', so its height in any cone representation is 1, reducing again to gluing in K.

In Lean: the face set, its affine independence and downward closure, the supporting facts for gluing (including the unique apex height), and the assembled complex with its underlying space:

open Geometry Set Finset
open scoped Topology
open _root_.FamiliesOfMapsB01

namespace Submission
namespace FamiliesOfMapsB01

variable {k : ℕ}

/-- The face set of the cone with apex `v` over a simplicial complex `K'`:
the faces of `K'`, the cones `insert v σ` over them, the apex `{v}`, and `∅`
(the last removed by `ofErase`). -/
def coneFaceSet (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ)) :
    Set (Finset (Fin k → ℝ)) :=
  K'.faces ∪ (insert v '' K'.faces) ∪ {{v}} ∪ {∅}

/-
Affine independence of every face of the cone face set.
-/
lemma coneFaceSet_indep (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ))
    (hv : v ∉ affineSpan ℝ K'.space) :
    ∀ s ∈ coneFaceSet v K', AffineIndependent ℝ ((↑) : s → (Fin k → ℝ)) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', AffineIndependent ℝ Subtype.val
  intro s hsk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.val
  by_cases h : s = ∅ ∨ s = {v} ∨ s ∈ K'.faces ∨ ∃ σ ∈ K'.faces, s = insert v σposk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:s = ∅ ∨ s = {v} ∨ s ∈ K'.faces ∨ ∃ σ ∈ K'.faces, s = insert v σ⊢ AffineIndependent ℝ Subtype.valnegk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:¬(s = ∅ ∨ s = {v} ∨ s ∈ K'.faces ∨ ∃ σ ∈ K'.faces, s = insert v σ)⊢ AffineIndependent ℝ Subtype.val;
  ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:s = ∅ ∨ s = {v} ∨ s ∈ K'.faces ∨ ∃ σ ∈ K'.faces, s = insert v σ⊢ AffineIndependent ℝ Subtype.val rcases h with ( rfl | rfl | h | ⟨ σ, hσ, rfl ⟩ )pos.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehs:∅ ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.valpos.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehs:{v} ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.valpos.inr.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:s ∈ K'.faces⊢ AffineIndependent ℝ Subtype.valpos.inr.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.val;
    ·pos.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehs:∅ ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.val exact affineIndependent_of_subsingleton _ _All goals completed! 🐙;
    ·pos.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehs:{v} ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.val exact affineIndependent_of_subsingleton _ _All goals completed! 🐙;
    ·pos.inr.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:s ∈ K'.faces⊢ AffineIndependent ℝ Subtype.val exact K'.indep hAll goals completed! 🐙;
    ·pos.inr.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'⊢ AffineIndependent ℝ Subtype.val by_cases h : v ∈ σposk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∈ σ⊢ AffineIndependent ℝ Subtype.valnegk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ AffineIndependent ℝ Subtype.val;
      ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∈ σ⊢ AffineIndependent ℝ Subtype.val exact False.elim <| hv <| subset_affineSpan ℝ _ <| K'.subset_space hσ hAll goals completed! 🐙;
      ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ AffineIndependent ℝ Subtype.val convert AffineIndependent.affineIndependent_of_notMem_span _ _neg.convert_10k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ ↥(insert v σ)neg.convert_11k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ AffineIndependent ℝ fun x => ↑↑xneg.convert_12k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ ↑?neg.convert_10✝ ∉ affineSpan ℝ (Subtype.val '' {x | x ≠ ?neg.convert_10✝});
        exact ⟨ v, Finset.mem_insert_self _ _ ⟩neg.convert_11k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ AffineIndependent ℝ fun x => ↑↑xneg.convert_12k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ ↑⟨v, ⋯⟩ ∉ affineSpan ℝ (Subtype.val '' {x | x ≠ ⟨v, ⋯⟩});
        ·neg.convert_11k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ AffineIndependent ℝ fun x => ↑↑x have := K'.indep hσneg.convert_11k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.val⊢ AffineIndependent ℝ fun x => ↑↑x;
          convert this.comp_embedding _h.e'_9.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx✝:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x✝ = (Subtype.val ∘ ⇑?neg.convert_11.convert_2✝) x✝neg.convert_11.convert_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.val⊢ { y // y ≠ ⟨v, ⋯⟩ } ↪ ↥σ;
          swapneg.convert_11.convert_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.val⊢ { y // y ≠ ⟨v, ⋯⟩ } ↪ ↥σh.e'_9.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx✝:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x✝ = (Subtype.val ∘ ⇑?neg.convert_11.convert_2✝) x✝;
          refine' ⟨ fun x => ⟨ x.val, _ ⟩, fun x y hxy => _ ⟩neg.convert_11.convert_2.refine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x ∈ σneg.convert_11.convert_2.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx:{ y // y ≠ ⟨v, ⋯⟩ }y:{ y // y ≠ ⟨v, ⋯⟩ }hxy:(fun x => ⟨↑↑x, ⋯⟩) x = (fun x => ⟨↑↑x, ⋯⟩) y⊢ x = yh.e'_9.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx✝:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x✝ = (Subtype.val ∘ ⇑{ toFun := fun x => ⟨↑↑x, ⋯⟩, inj' := ⋯ }) x✝;
          grindneg.convert_11.convert_2.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx:{ y // y ≠ ⟨v, ⋯⟩ }y:{ y // y ≠ ⟨v, ⋯⟩ }hxy:(fun x => ⟨↑↑x, ⋯⟩) x = (fun x => ⟨↑↑x, ⋯⟩) y⊢ x = yh.e'_9.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx✝:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x✝ = (Subtype.val ∘ ⇑{ toFun := fun x => ⟨↑↑x, ⋯⟩, inj' := ⋯ }) x✝;
          grindh.e'_9.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σthis:AffineIndependent ℝ Subtype.valx✝:{ y // y ≠ ⟨v, ⋯⟩ }⊢ ↑↑x✝ = (Subtype.val ∘ ⇑{ toFun := fun x => ⟨↑↑x, ⋯⟩, inj' := ⋯ }) x✝;
          rflAll goals completed! 🐙;
        ·neg.convert_12k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ ↑⟨v, ⋯⟩ ∉ affineSpan ℝ (Subtype.val '' {x | x ≠ ⟨v, ⋯⟩}) convert hv using 1h.e'_1.ak:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ ↑⟨v, ⋯⟩ ∈ affineSpan ℝ (Subtype.val '' {x | x ≠ ⟨v, ⋯⟩}) ↔ v ∈ affineSpan ℝ K'.space;
          simp +decide [ Set.image, Subtype.ext_iff ]h.e'_1.ak:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ v ∈ affineSpan ℝ {x | ¬x = v ∧ (x = v ∨ x ∈ σ)} ↔ v ∈ affineSpan ℝ K'.space;
          rw [ show { x : Fin k → ℝ | ¬x = v ∧ ( x = v ∨ x ∈ σ ) } = σ by ext x; by_cases hx : x = v <;> aesop ]h.e'_1.ak:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaceσ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faceshs:insert v σ ∈ coneFaceSet v K'h:v ∉ σ⊢ v ∈ affineSpan ℝ ↑σ ↔ v ∈ affineSpan ℝ K'.space;
          exact iff_of_false ( fun h' => hv <| affineSpan_mono ℝ ( K'.subset_space hσ ) h' ) hvAll goals completed! 🐙;
  ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'h:¬(s = ∅ ∨ s = {v} ∨ s ∈ K'.faces ∨ ∃ σ ∈ K'.faces, s = insert v σ)⊢ AffineIndependent ℝ Subtype.val grind +localsAll goals completed! 🐙

/-
The cone face set is a lower set (downward closed under `⊆`).
-/
lemma coneFaceSet_isLowerSet (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ)) :
    IsLowerSet (coneFaceSet v K') := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)⊢ IsLowerSet (coneFaceSet v K')
  intro a bk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)⊢ b ≤ a → a ∈ coneFaceSet v K' → b ∈ coneFaceSet v K' habk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ≤ a⊢ a ∈ coneFaceSet v K' → b ∈ coneFaceSet v K' hak:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ≤ aha:a ∈ coneFaceSet v K'⊢ b ∈ coneFaceSet v K';
  simp_all +decide [ coneFaceSet ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ aha:a = ∅ ∨ a = {v} ∨ a ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = a⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b;
  rcases ha with ( rfl | rfl | ha | ⟨ s, hs, rfl ⟩ )inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = binr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ {v}⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = binr.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ aha:a ∈ K'.faces⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = binr.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v s⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b;
  ·inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b aesopAll goals completed! 🐙;
  ·inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ {v}⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b rw [ Finset.subset_singleton_iff ] at habinr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b = ∅ ∨ b = {v}⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b ; aesopAll goals completed! 🐙;
  ·inr.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)a:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ⊆ aha:a ∈ K'.faces⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b grind +suggestionsAll goals completed! 🐙;
  ·inr.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v s⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b by_cases hv : v ∈ bposk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ b⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = bnegk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∉ b⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b;
    ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ b⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b have h_erase : b.erase v ⊆ s := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)⊢ IsLowerSet (coneFaceSet v K')
        grindAll goals completed! 🐙;
      by_cases h_erase_empty : b.erase v = ∅posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ bh_erase:b.erase v ⊆ sh_erase_empty:b.erase v = ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = bnegk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ bh_erase:b.erase v ⊆ sh_erase_empty:¬b.erase v = ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b;
      ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ bh_erase:b.erase v ⊆ sh_erase_empty:b.erase v = ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b grindAll goals completed! 🐙;
      ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ bh_erase:b.erase v ⊆ sh_erase_empty:¬b.erase v = ∅⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b exact Or.inr <| Or.inr <| Or.inr <| ⟨ b.erase v, K'.down_closed hs h_erase <| Finset.nonempty_of_ne_empty h_erase_empty, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∈ bh_erase:b.erase v ⊆ sh_erase_empty:¬b.erase v = ∅⊢ insert v (b.erase v) = b rw [ Finset.insert_erase hv ]All goals completed! 🐙 ⟩;
    ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)b:Finset (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshab:b ⊆ insert v shv:v ∉ b⊢ b = ∅ ∨ b = {v} ∨ b ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = b grind +suggestionsAll goals completed! 🐙

/-
The convex hull of a face is contained in the affine span of the whole space.
-/
lemma face_convexHull_subset_affineSpan (K' : SimplicialComplex ℝ (Fin k → ℝ))
    {σ : Finset (Fin k → ℝ)} (hσ : σ ∈ K'.faces) :
    convexHull ℝ (σ : Set (Fin k → ℝ)) ⊆ (affineSpan ℝ K'.space : Set (Fin k → ℝ)) := byk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces⊢ (convexHull ℝ) ↑σ ⊆ ↑(affineSpan ℝ K'.space)
  refine' convexHull_min _ _refine'_1k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces⊢ ↑σ ⊆ ↑(affineSpan ℝ K'.space)refine'_2k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces⊢ Convex ℝ ↑(affineSpan ℝ K'.space);
  ·refine'_1k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces⊢ ↑σ ⊆ ↑(affineSpan ℝ K'.space) exact fun x hx => subset_affineSpan ℝ _ <| K'.subset_space hσ hxAll goals completed! 🐙;
  ·refine'_2k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces⊢ Convex ℝ ↑(affineSpan ℝ K'.space) exact (affineSpan ℝ K'.space).convexAll goals completed! 🐙

/-
**Unique apex height.** If `v` lies off `affineSpan K'.space`, then in any segment
representation `(1-a)•v + a•b` with base `b` in that affine span, the height `a` is
determined: two such representations forcing the same point have the same `a`.
-/
lemma apex_param_unique (K' : SimplicialComplex ℝ (Fin k → ℝ))
    {v : Fin k → ℝ} (hv : v ∉ affineSpan ℝ K'.space)
    {a a' : ℝ} {b b' : Fin k → ℝ}
    (hb : b ∈ affineSpan ℝ K'.space) (hb' : b' ∈ affineSpan ℝ K'.space)
    (h : (1 - a) • v + a • b = (1 - a') • v + a' • b') : a = a' := byk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝhv:v ∉ affineSpan ℝ K'.spacea:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'⊢ a = a'
  contrapose! hvk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'⊢ v ∈ affineSpan ℝ K'.space;
  -- Rearrange h to get $(a' - a) • v = a' • b' - a • b$.
  have h_rearrange : (a' - a) • v = a' • b' - a • b := byk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝhv:v ∉ affineSpan ℝ K'.spacea:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'⊢ a = a'
    exact eq_of_sub_eq_zero ( byk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'⊢ (a' - a) • v - (a' • b' - a • b) = 0 ext xhk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'x:Fin k⊢ ((a' - a) • v - (a' • b' - a • b)) x = 0 x; have := congr_fun h xhk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'x:Fin kthis:((1 - a) • v + a • b) x = ((1 - a') • v + a' • b') x⊢ ((a' - a) • v - (a' • b' - a • b)) x = 0 x; norm_num at *hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'x:Fin kthis:(1 - a) * v x + a * b x = (1 - a') * v x + a' * b' x⊢ (a' - a) * v x - (a' * b' x - a * b x) = 0; linarithAll goals completed! 🐙 );
  convert AffineSubspace.smul_vsub_vadd_mem _ _ hb' hb hb using 1h.e'_1k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • b⊢ v = ?m.165 • (b' -ᵥ b) +ᵥ bk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • b⊢ ℝ;
  swapk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • b⊢ ℝh.e'_1k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • b⊢ v = ?m.165 • (b' -ᵥ b) +ᵥ b;
  exact ( a' - a ) ⁻¹ * a'h.e'_1k:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • b⊢ v = ((a' - a)⁻¹ * a') • (b' -ᵥ b) +ᵥ b;
  ext ih.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin k⊢ v i = (((a' - a)⁻¹ * a') • (b' -ᵥ b) +ᵥ b) i; have := congr_fun h_rearrange ih.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:a ≠ a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:((a' - a) • v) i = (a' • b' - a • b) i⊢ v i = (((a' - a)⁻¹ * a') • (b' -ᵥ b) +ᵥ b) i; norm_num at *h.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ v i = (a' - a)⁻¹ * a' * (b' i - b i) + b i; rw [ inv_mul_eq_div, div_mul_eq_mul_div, div_add', eq_div_iff ]h.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ v i * (a' - a) = a' * (b' i - b i) + b i * (a' - a)h.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ a' - a ≠ 0h.e'_1.h.hck:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ a' - a ≠ 0 <;>h.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ v i * (a' - a) = a' * (b' i - b i) + b i * (a' - a)h.e'_1.hk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ a' - a ≠ 0h.e'_1.h.hck:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b i⊢ a' - a ≠ 0 cases lt_or_gt_of_ne hvh.e'_1.h.hc.inlk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a < a'⊢ a' - a ≠ 0h.e'_1.h.hc.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a' < a⊢ a' - a ≠ 0 <;>h.e'_1.h.inlk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a < a'⊢ v i * (a' - a) = a' * (b' i - b i) + b i * (a' - a)h.e'_1.h.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a' < a⊢ v i * (a' - a) = a' * (b' i - b i) + b i * (a' - a)h.e'_1.h.inlk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a < a'⊢ a' - a ≠ 0h.e'_1.h.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a' < a⊢ a' - a ≠ 0h.e'_1.h.hc.inlk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a < a'⊢ a' - a ≠ 0h.e'_1.h.hc.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)v:Fin k → ℝa:ℝa':ℝb:Fin k → ℝb':Fin k → ℝhb:b ∈ affineSpan ℝ K'.spacehb':b' ∈ affineSpan ℝ K'.spaceh:(1 - a) • v + a • b = (1 - a') • v + a' • b'hv:¬a = a'h_rearrange:(a' - a) • v = a' • b' - a • bi:Fin kthis:(a' - a) * v i = a' * b' i - a * b ih✝:a' < a⊢ a' - a ≠ 0 nlinarithAll goals completed! 🐙;

set_option maxHeartbeats 4000000 in
/-- The intersection (glue-nicely) condition for the cone face set. -/
lemma coneFaceSet_inter (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ))
    (hv : v ∉ affineSpan ℝ K'.space) :
    ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K',
      convexHull ℝ (s : Set (Fin k → ℝ)) ∩ convexHull ℝ (t : Set (Fin k → ℝ)) ⊆
        convexHull ℝ ((s : Set (Fin k → ℝ)) ∩ (t : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
  intro s hsk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K'⊢ ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t) tk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K't:Finset (Fin k → ℝ)⊢ t ∈ coneFaceSet v K' → (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t) htk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ coneFaceSet v K't:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t);
  rcases hs with ( ( hs | hs ) | hs | hs )inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'hs:s ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'hs:s ∈ {{v}}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t) <;>inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'hs:s ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'hs:s ∈ {{v}}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ coneFaceSet v K'⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t) rcases ht with ( ( ht | ht ) | ht | ht )inr.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t)inr.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ {{v}}⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t)inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) (↑∅ ∩ ↑∅) <;>inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∪ insert v '' K'.facesht:t ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∪ insert v '' K'.facesht:t ∈ {{v}}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) (↑s ∩ ↑∅)inl.inr.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ {{v}}ht:t ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inr.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ {{v}}ht:t ∈ {{v}}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)inl.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ {{v}}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) (↑s ∩ ↑∅)inr.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∪ insert v '' K'.faces⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t)inr.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ {{v}}⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑∅ ∩ ↑t)inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ (convexHull ℝ) ↑∅ ∩ (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) (↑∅ ∩ ↑∅) simp_all +decide [ Set.subset_def ]All goals completed! 🐙;
  ·inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = sht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = t⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑t → x ∈ (convexHull ℝ) (↑s ∩ ↑t) rcases hs with ( hs | ⟨ x, hx, rfl ⟩ )inl.inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = ths:s ∈ K'.faces⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑t → x ∈ (convexHull ℝ) (↑s ∩ ↑t)inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = tx:Finset (Fin k → ℝ)hx:x ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x), x_1 ∈ (convexHull ℝ) ↑t → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑t) <;>inl.inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = ths:s ∈ K'.faces⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑t → x ∈ (convexHull ℝ) (↑s ∩ ↑t)inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = tx:Finset (Fin k → ℝ)hx:x ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x), x_1 ∈ (convexHull ℝ) ↑t → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑t) rcases ht with ( ht | ⟨ y, hy, rfl ⟩ )inl.inl.inl.inl.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x), x_1 ∈ (convexHull ℝ) ↑t → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑t)inl.inl.inl.inl.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x),
  x_1 ∈ (convexHull ℝ) ↑(insert v y) → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y));
    ·inl.inl.inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.facesht:t ∈ K'.faces⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑t → x ∈ (convexHull ℝ) (↑s ∩ ↑t) have := K'.convexHull_inter_convexHull hs htinl.inl.inl.inl.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.facesht:t ∈ K'.facesthis:(convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t = (convexHull ℝ) (↑s ∩ ↑t)⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑t → x ∈ (convexHull ℝ) (↑s ∩ ↑t);
      exact fun x hx₁ hx₂ => this ▸ ⟨ hx₁, hx₂ ⟩All goals completed! 🐙;
    ·inl.inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.faces⊢ ∀ x ∈ (convexHull ℝ) ↑s, x ∈ (convexHull ℝ) ↑(insert v y) → x ∈ (convexHull ℝ) (↑s ∩ ↑(insert v y)) intro x hx₁inl.inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑s⊢ x ∈ (convexHull ℝ) ↑(insert v y) → x ∈ (convexHull ℝ) (↑s ∩ ↑(insert v y)) hx₂inl.inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)⊢ x ∈ (convexHull ℝ) (↑s ∩ ↑(insert v y));
      -- Since $x \in \text{convexHull}(\text{insert } v y)$, we have $x = (1 - a) • v + a • b$ for some $a \in [0, 1]$ and $b \in \text{convexHull}(y)$.
      obtain ⟨a, ha, b, hb, hx⟩ : ∃ a ∈ Set.Icc (0 : ℝ) 1, ∃ b ∈ convexHull ℝ (y : Set (Fin k → ℝ)), x = (1 - a) • v + a • b := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)⊢ ∃ a ∈ Set.Icc 0 1, ∃ b ∈ (convexHull ℝ) ↑y, x = (1 - a) • v + a • b
        have h_convex_hull : convexHull ℝ (insert v y : Set (Fin k → ℝ)) = convexJoin ℝ {v} (convexHull ℝ (y : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)⊢ ∃ a ∈ Set.Icc 0 1, ∃ b ∈ (convexHull ℝ) ↑y, x = (1 - a) • v + a • b
          by_cases hy : y.Nonemptyposk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy✝:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)hy:y.Nonempty⊢ (convexHull ℝ) (insert v ↑y) = convexJoin ℝ {v} ((convexHull ℝ) ↑y)negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy✝:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)hy:¬y.Nonempty⊢ (convexHull ℝ) (insert v ↑y) = convexJoin ℝ {v} ((convexHull ℝ) ↑y) <;>posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy✝:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)hy:y.Nonempty⊢ (convexHull ℝ) (insert v ↑y) = convexJoin ℝ {v} ((convexHull ℝ) ↑y)negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy✝:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)hy:¬y.Nonempty⊢ (convexHull ℝ) (insert v ↑y) = convexJoin ℝ {v} ((convexHull ℝ) ↑y) simp_all +decide [ convexHull_insert ]negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)x:Fin k → ℝhy✝:∅ ∈ K'.faceshx₁:v ∈ (convexHull ℝ) ↑shx₂:x = vhy:y = ∅⊢ False;
          exact absurd ‹∅ ∈ K'.faces› ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)x:Fin k → ℝhy✝:∅ ∈ K'.faceshx₁:v ∈ (convexHull ℝ) ↑shx₂:x = vhy:y = ∅⊢ ∅ ∉ K'.faces simpa using K'.empty_notMemAll goals completed! 🐙 );
        simp_all +decide [ convexJoin ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:∃ i ∈ (convexHull ℝ) ↑y, x ∈ segment ℝ v ih_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1⊢ ∃ a, (0 ≤ a ∧ a ≤ 1) ∧ ∃ b ∈ (convexHull ℝ) ↑y, x = (1 - a) • v + a • b;
        rcases hx₂ with ⟨ b, hb, hx₂ ⟩k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑sh_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx₂:x ∈ segment ℝ v b⊢ ∃ a, (0 ≤ a ∧ a ≤ 1) ∧ ∃ b ∈ (convexHull ℝ) ↑y, x = (1 - a) • v + a • b ; rw [ segment_eq_image ] at hx₂k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑sh_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx₂:x ∈ (fun θ => (1 - θ) • v + θ • b) '' Set.Icc 0 1⊢ ∃ a, (0 ≤ a ∧ a ≤ 1) ∧ ∃ b ∈ (convexHull ℝ) ↑y, x = (1 - a) • v + a • b; obtain ⟨ a, ha, rfl ⟩ := hx₂k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesh_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑ya:ℝha:a ∈ Set.Icc 0 1hx₁:(fun θ => (1 - θ) • v + θ • b) a ∈ (convexHull ℝ) ↑s⊢ ∃ a_1, (0 ≤ a_1 ∧ a_1 ≤ 1) ∧ ∃ b_1 ∈ (convexHull ℝ) ↑y, (fun θ => (1 - θ) • v + θ • b) a = (1 - a_1) • v + a_1 • b_1; exact ⟨ a, ⟨ byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesh_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑ya:ℝha:a ∈ Set.Icc 0 1hx₁:(fun θ => (1 - θ) • v + θ • b) a ∈ (convexHull ℝ) ↑s⊢ 0 ≤ a linarith [ Set.mem_Icc.mp ha ]All goals completed! 🐙, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesh_convex_hull:(convexHull ℝ) (insert v ↑y) = ⋃ y_1 ∈ (convexHull ℝ) ↑y, segment ℝ v y_1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑ya:ℝha:a ∈ Set.Icc 0 1hx₁:(fun θ => (1 - θ) • v + θ • b) a ∈ (convexHull ℝ) ↑s⊢ a ≤ 1 linarith [ Set.mem_Icc.mp ha ]All goals completed! 🐙 ⟩, b, hb, rfl ⟩ ;
      have h_a_one : a = 1 := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        have h_a_one : a = 1 := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
          have h_b_in_affineSpan : b ∈ affineSpan ℝ K'.space := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
            exact face_convexHull_subset_affineSpan K' hy hbAll goals completed! 🐙
          have h_x_in_affineSpan : x ∈ affineSpan ℝ K'.space := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
            exact face_convexHull_subset_affineSpan K' hs hx₁All goals completed! 🐙
          have h_a_one : (1 - a) • v + a • b ∈ affineSpan ℝ K'.space := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
            aesopAll goals completed! 🐙;
          contrapose! hvk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1⊢ v ∈ affineSpan ℝ K'.space;
          convert AffineSubspace.vadd_mem_of_mem_direction ( show ( 1 / ( 1 - a ) ) • ( ( 1 - a ) • v + a • b - b ) ∈ ( affineSpan ℝ K'.space ).direction from ?_ ) h_b_in_affineSpan using 1h.e'_5k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1⊢ v = (1 / (1 - a)) • ((1 - a) • v + a • b - b) +ᵥ bk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1⊢ (1 / (1 - a)) • ((1 - a) • v + a • b - b) ∈ (affineSpan ℝ K'.space).direction;
          ·h.e'_5k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1⊢ v = (1 / (1 - a)) • ((1 - a) • v + a • b - b) +ᵥ b ext ih.e'_5.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1i:Fin k⊢ v i = ((1 / (1 - a)) • ((1 - a) • v + a • b - b) +ᵥ b) i; simp +decide [ hv, sub_ne_zero, smul_smul ]h.e'_5.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1i:Fin k⊢ v i = (1 - a)⁻¹ * ((1 - a) * v i + a * b i - b i) + b i ; Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ringh.e'_5.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1i:Fin k⊢ v i = -(a * (1 - a)⁻¹ * v i) + a * (1 - a)⁻¹ * b i + (1 - a)⁻¹ * v i - (1 - a)⁻¹ * b i + b i;
            grindAll goals completed! 🐙;
          ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝhx₁:x ∈ (convexHull ℝ) ↑shx₂:x ∈ (convexHull ℝ) ↑(insert v y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑yhx:x = (1 - a) • v + a • bh_b_in_affineSpan:b ∈ affineSpan ℝ K'.spaceh_x_in_affineSpan:x ∈ affineSpan ℝ K'.spaceh_a_one:(1 - a) • v + a • b ∈ affineSpan ℝ K'.spacehv:a ≠ 1⊢ (1 / (1 - a)) • ((1 - a) • v + a • b - b) ∈ (affineSpan ℝ K'.space).direction exact Submodule.smul_mem _ _ ( AffineSubspace.vsub_mem_direction h_a_one h_b_in_affineSpan )All goals completed! 🐙;
        exact h_a_oneAll goals completed! 🐙;
      simp_all +decide [ convexHull_insert ]inl.inl.inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝa:ℝb:Fin k → ℝhx₁:b ∈ (convexHull ℝ) ↑shx₂:b ∈ (convexHull ℝ) (insert v ↑y)hb:b ∈ (convexHull ℝ) ↑yhx:x = bh_a_one:a = 1⊢ b ∈ (convexHull ℝ) (↑s ∩ insert v ↑y);
      have h_inter : b ∈ convexHull ℝ (s ∩ y : Set (Fin k → ℝ)) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        have := K'.convexHull_inter_convexHull hs hyk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝa:ℝb:Fin k → ℝhx₁:b ∈ (convexHull ℝ) ↑shx₂:b ∈ (convexHull ℝ) (insert v ↑y)hb:b ∈ (convexHull ℝ) ↑yhx:x = bh_a_one:a = 1this:(convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑y = (convexHull ℝ) (↑s ∩ ↑y)⊢ b ∈ (convexHull ℝ) (↑s ∩ ↑y);
        exact this ▸ ⟨ hx₁, hb ⟩All goals completed! 🐙;
      exact convexHull_mono ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)hs:s ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesx:Fin k → ℝa:ℝb:Fin k → ℝhx₁:b ∈ (convexHull ℝ) ↑shx₂:b ∈ (convexHull ℝ) (insert v ↑y)hb:b ∈ (convexHull ℝ) ↑yhx:x = bh_a_one:a = 1h_inter:b ∈ (convexHull ℝ) (↑s ∩ ↑y)⊢ ↑s ∩ ↑y ⊆ ↑s ∩ insert v ↑y aesop_catAll goals completed! 🐙 ) h_inter;
    ·inl.inl.inl.inl.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x), x_1 ∈ (convexHull ℝ) ↑t → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑t) have h_convexHull_insert : (convexHull ℝ (insert v x : Set (Fin k → ℝ))) = convexJoin ℝ {v} (convexHull ℝ (x : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        rw [ convexHull_insert ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.faces⊢ (↑x).Nonempty ; aesop: failed to prove the goal after exhaustive search.aesopk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.faces⊢ x.Nonempty;
        exact Finset.nonempty_of_ne_empty ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.faces⊢ x ≠ ∅ rintro rflk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)ht:t ∈ K'.faceshx:∅ ∈ K'.faces⊢ False; exact K'.empty_notMem hxAll goals completed! 🐙 );
      simp_all +decide [ convexJoin_singleton_left, segment_eq_image ]inl.inl.inl.inl.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1⊢ ∀ (x_1 x_2 : Fin k → ℝ),
  x_2 ∈ (convexHull ℝ) ↑x →
    ∀ (x_3 : ℝ),
      0 ≤ x_3 →
        x_3 ≤ 1 → (1 - x_3) • v + x_3 • x_2 = x_1 → x_1 ∈ (convexHull ℝ) ↑t → x_1 ∈ (convexHull ℝ) (insert v ↑x ∩ ↑t);
      rintro _ y hy a ha₁ ha₂ rfl hy'inl.inl.inl.inl.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ (1 - a) • v + a • y ∈ (convexHull ℝ) (insert v ↑x ∩ ↑t);
      have h_apex_param_unique : a = 1 := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        apply apex_param_unique K' hvhbk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ ?m.1068 ∈ affineSpan ℝ K'.spacehb'k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ ?m.1069 ∈ affineSpan ℝ K'.spacehk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ (1 - a) • v + a • ?m.1068 = (1 - 1) • v + 1 • ?m.1069k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ Fin k → ℝk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ Fin k → ℝ;
        exact face_convexHull_subset_affineSpan K' hx hyhb'k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ ?m.1069 ∈ affineSpan ℝ K'.spacehk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ (1 - a) • v + a • y = (1 - 1) • v + 1 • ?m.1069k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ Fin k → ℝ;
        convert face_convexHull_subset_affineSpan K' ht hy' using 1hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝha₁:0 ≤ aha₂:a ≤ 1hy':(1 - a) • v + a • y ∈ (convexHull ℝ) ↑t⊢ (1 - a) • v + a • y = (1 - 1) • v + 1 • ((1 - a) • v + a • y);
        norm_numAll goals completed! 🐙;
      simp_all +decide [ convexHull_insert ]inl.inl.inl.inl.inr.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝhy':y ∈ (convexHull ℝ) ↑th_apex_param_unique:a = 1⊢ y ∈ (convexHull ℝ) (insert v ↑x ∩ ↑t);
      have h_convexHull_inter : (convexHull ℝ (x : Set (Fin k → ℝ))) ∩ (convexHull ℝ (t : Set (Fin k → ℝ))) ⊆ (convexHull ℝ (x ∩ t : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        grind +suggestionsAll goals completed! 🐙;
      exact h_convexHull_inter ⟨ hy, hy' ⟩ |> fun h => convexHull_mono ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacet:Finset (Fin k → ℝ)x:Finset (Fin k → ℝ)hx:x ∈ K'.facesht:t ∈ K'.facesh_convexHull_insert:(convexHull ℝ) (insert v ↑x) = ⋃ y ∈ (convexHull ℝ) ↑x, (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1y:Fin k → ℝhy:y ∈ (convexHull ℝ) ↑xa:ℝhy':y ∈ (convexHull ℝ) ↑th_apex_param_unique:a = 1h_convexHull_inter:(convexHull ℝ) ↑x ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑x ∩ ↑t)h:y ∈ (convexHull ℝ) (↑x ∩ ↑t)⊢ ↑x ∩ ↑t ⊆ insert v ↑x ∩ ↑t aesop_catAll goals completed! 🐙 ) h;
    ·inl.inl.inl.inl.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.faces⊢ ∀ x_1 ∈ (convexHull ℝ) ↑(insert v x),
  x_1 ∈ (convexHull ℝ) ↑(insert v y) → x_1 ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y)) intro z hz₁inl.inl.inl.inl.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)⊢ z ∈ (convexHull ℝ) ↑(insert v y) → z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y)) hz₂inl.inl.inl.inl.inr.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)⊢ z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y))
      have hz : z ∈ convexJoin ℝ {v} (convexHull ℝ (x : Set (Fin k → ℝ))) ∧ z ∈ convexJoin ℝ {v} (convexHull ℝ (y : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        simp_all +decide [ convexHull_insert, convexJoin_singleton_left ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) (insert v ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ (∃ i ∈ (convexHull ℝ) ↑x, z ∈ segment ℝ v i) ∧ ∃ i ∈ (convexHull ℝ) ↑y, z ∈ segment ℝ v i;
        rw [ convexHull_insert ] at hz₁ hz₂k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hz₂:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)⊢ (∃ i ∈ (convexHull ℝ) ↑x, z ∈ segment ℝ v i) ∧ ∃ i ∈ (convexHull ℝ) ↑y, z ∈ segment ℝ v ik:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ (↑y).Nonemptyk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) (insert v ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ (↑x).Nonempty;
        ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hz₂:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)⊢ (∃ i ∈ (convexHull ℝ) ↑x, z ∈ segment ℝ v i) ∧ ∃ i ∈ (convexHull ℝ) ↑y, z ∈ segment ℝ v i simp_all +decide [ convexJoin ]All goals completed! 🐙;
        ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ (↑y).Nonempty exact Finset.nonempty_of_ne_empty ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ y ≠ ∅ rintro rflk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesz:Fin k → ℝhz₁:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x)hy:∅ ∈ K'.faceshz₂:z ∈ (convexHull ℝ) (insert v ↑∅)⊢ False; exact K'.empty_notMem hyAll goals completed! 🐙 );
        ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) (insert v ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ (↑x).Nonempty exact Finset.nonempty_of_ne_empty ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) (insert v ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)⊢ x ≠ ∅ rintro rflk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacey:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₂:z ∈ (convexHull ℝ) (insert v ↑y)hx:∅ ∈ K'.faceshz₁:z ∈ (convexHull ℝ) (insert v ↑∅)⊢ False; simp_all +decide [ SimplicialComplex.empty_notMem ]All goals completed! 🐙 );
      obtain ⟨a, ha, b, hb, hab⟩ : ∃ a ∈ Set.Icc (0 : ℝ) 1, ∃ b ∈ convexHull ℝ (x : Set (Fin k → ℝ)), z = (1 - a) • v + a • b := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)⊢ ∃ a ∈ Set.Icc 0 1, ∃ b ∈ (convexHull ℝ) ↑x, z = (1 - a) • v + a • b
        simp_all +decide [ segment_eq_image ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) (insert v ↑x)hz₂:z ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = z) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = z⊢ ∃ a, (0 ≤ a ∧ a ≤ 1) ∧ ∃ b ∈ (convexHull ℝ) ↑x, z = (1 - a) • v + a • b;
        rcases hz.1 with ⟨ b, hb, a, ha, rfl ⟩k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesb:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xa:ℝha:0 ≤ a ∧ a ≤ 1hz₁:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • b) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • b⊢ ∃ a_1, (0 ≤ a_1 ∧ a_1 ≤ 1) ∧ ∃ b_1 ∈ (convexHull ℝ) ↑x, (1 - a) • v + a • b = (1 - a_1) • v + a_1 • b_1 ; exact ⟨ a, ha, b, hb, rfl ⟩All goals completed! 🐙
      obtain ⟨a', ha', b', hb', hab'⟩ : ∃ a' ∈ Set.Icc (0 : ℝ) 1, ∃ b' ∈ convexHull ℝ (y : Set (Fin k → ℝ)), z = (1 - a') • v + a' • b' := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • b⊢ ∃ a' ∈ Set.Icc 0 1, ∃ b' ∈ (convexHull ℝ) ↑y, z = (1 - a') • v + a' • b'
        simp_all +decide [ segment_eq_image ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝhz₁:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • b) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • bha:0 ≤ a ∧ a ≤ 1hb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • b⊢ ∃ a', (0 ≤ a' ∧ a' ≤ 1) ∧ ∃ b' ∈ (convexHull ℝ) ↑y, (1 - a) • v + a • b = (1 - a') • v + a' • b';
        rcases hz.2 with ⟨ i, hi, x, hx, hx' ⟩k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex✝:Finset (Fin k → ℝ)hx✝:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝhz₁:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a) • v + a • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • b) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, ∃ x, (0 ≤ x ∧ x ≤ 1) ∧ (1 - x) • v + x • i = (1 - a) • v + a • bha:0 ≤ a ∧ a ≤ 1hb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • bi:Fin k → ℝhi:i ∈ (convexHull ℝ) ↑yx:ℝhx:0 ≤ x ∧ x ≤ 1hx':(1 - x) • v + x • i = (1 - a) • v + a • b⊢ ∃ a', (0 ≤ a' ∧ a' ≤ 1) ∧ ∃ b' ∈ (convexHull ℝ) ↑y, (1 - a) • v + a • b = (1 - a') • v + a' • b' ; exact ⟨ x, hx, i, hi, hx'.symm ⟩All goals completed! 🐙 ;
      have h_eq : a = a' := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
        apply apex_param_unique K' hvhbk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ ?m.1826 ∈ affineSpan ℝ K'.spacehb'k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ ?m.1827 ∈ affineSpan ℝ K'.spacehk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ (1 - a) • v + a • ?m.1826 = (1 - a') • v + a' • ?m.1827k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ Fin k → ℝk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ Fin k → ℝ;
        exact face_convexHull_subset_affineSpan K' hx hbhb'k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ ?m.1827 ∈ affineSpan ℝ K'.spacehk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ (1 - a) • v + a • b = (1 - a') • v + a' • ?m.1827k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ Fin k → ℝ;
        exact face_convexHull_subset_affineSpan K' hy hb'hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'⊢ (1 - a) • v + a • b = (1 - a') • v + a' • b';
        rw [ ← hab, ← hab' ]All goals completed! 🐙;
      by_cases ha : a = 0posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha✝:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'h_eq:a = a'ha:a = 0⊢ z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y))negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha✝:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'h_eq:a = a'ha:¬a = 0⊢ z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y)) <;>posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha✝:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'h_eq:a = a'ha:a = 0⊢ z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y))negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝhz₁:z ∈ (convexHull ℝ) ↑(insert v x)hz₂:z ∈ (convexHull ℝ) ↑(insert v y)hz:z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑x) ∧ z ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑y)a:ℝha✝:a ∈ Set.Icc 0 1b:Fin k → ℝhb:b ∈ (convexHull ℝ) ↑xhab:z = (1 - a) • v + a • ba':ℝha':a' ∈ Set.Icc 0 1b':Fin k → ℝhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • b'h_eq:a = a'ha:¬a = 0⊢ z ∈ (convexHull ℝ) (↑(insert v x) ∩ ↑(insert v y)) simp_all +decide [ convexHull_insert ]negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq:a = a'ha:¬a' = 0⊢ (1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x ∩ insert v ↑y);
      ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:a' • b' = a' • bhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq:0 = a'ha:a = a'⊢ (1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x ∩ insert v ↑y) exact subset_convexHull ℝ _ ( byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:a' • b' = a' • bhb':b' ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq:0 = a'ha:a = a'⊢ (1 - a') • v + a' • b ∈ insert v ↑x ∩ insert v ↑y aesopAll goals completed! 🐙 );
      ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq:a = a'ha:¬a' = 0⊢ (1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x ∩ insert v ↑y) have h_eq : b ∈ convexHull ℝ (x ∩ y : Set (Fin k → ℝ)) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
          have := K'.convexHull_inter_convexHull hx hyk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq:a = a'ha:¬a' = 0this:(convexHull ℝ) ↑x ∩ (convexHull ℝ) ↑y = (convexHull ℝ) (↑x ∩ ↑y)⊢ b ∈ (convexHull ℝ) (↑x ∩ ↑y);
          exact this ▸ ⟨ hb, hb' ⟩All goals completed! 🐙;
        have h_eq : (1 - a') • v + a' • b ∈ convexHull ℝ (insert v (x ∩ y : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.space⊢ ∀ s ∈ coneFaceSet v K', ∀ t ∈ coneFaceSet v K', (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
          rw [ convexHull_insert ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (1 - a') • v + a' • b ∈ convexJoin ℝ {v} ((convexHull ℝ) (↑x ∩ ↑y))k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (↑x ∩ ↑y).Nonempty;
          ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (1 - a') • v + a' • b ∈ convexJoin ℝ {v} ((convexHull ℝ) (↑x ∩ ↑y)) simp +decide [ convexJoin ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ ∃ i ∈ (convexHull ℝ) (↑x ∩ ↑y), (1 - a') • v + a' • b ∈ segment ℝ v i;
            exact ⟨ b, h_eq, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (1 - a') • v + a' • b ∈ segment ℝ v b rw [ segment_eq_image ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (1 - a') • v + a' • b ∈ (fun θ => (1 - θ) • v + θ • b) '' Set.Icc 0 1 ; exact ⟨ a', ⟨ byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ 0 ≤ a' linarithAll goals completed! 🐙, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ a' ≤ 1 linarithAll goals completed! 🐙 ⟩, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (fun θ => (1 - θ) • v + θ • b) a' = (1 - a') • v + a' • b simp +decide [ add_comm ]All goals completed! 🐙 ⟩ ⟩;
          ·k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:b ∈ (convexHull ℝ) (↑x ∩ ↑y)⊢ (↑x ∩ ↑y).Nonempty contrapose! h_eqk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝:a = a'ha:¬a' = 0h_eq:↑x ∩ ↑y = ∅⊢ b ∉ (convexHull ℝ) (↑x ∩ ↑y); aesopAll goals completed! 🐙;
        convert h_eq using 1h.e'_4k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝¹:a = a'ha:¬a' = 0h_eq✝:b ∈ (convexHull ℝ) (↑x ∩ ↑y)h_eq:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v (↑x ∩ ↑y))⊢ (convexHull ℝ) (insert v ↑x ∩ insert v ↑y) = (convexHull ℝ) (insert v (↑x ∩ ↑y));
        congr with xh.e'_4.h.e_6.h.hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacex✝:Finset (Fin k → ℝ)hx:x ∈ K'.facesy:Finset (Fin k → ℝ)hy:y ∈ K'.facesz:Fin k → ℝa:ℝb:Fin k → ℝa':ℝb':Fin k → ℝhz₁:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑x)hz₂:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v ↑y)hz:(∃ i ∈ (convexHull ℝ) ↑x, (1 - a') • v + a' • b ∈ segment ℝ v i) ∧
  ∃ i ∈ (convexHull ℝ) ↑y, (1 - a') • v + a' • b ∈ segment ℝ v ihb:b ∈ (convexHull ℝ) ↑xhab:b' = bha':0 ≤ a' ∧ a' ≤ 1hb':b ∈ (convexHull ℝ) ↑yhab':z = (1 - a') • v + a' • bh_eq✝¹:a = a'ha:¬a' = 0h_eq✝:b ∈ (convexHull ℝ) (↑x ∩ ↑y)h_eq:(1 - a') • v + a' • b ∈ (convexHull ℝ) (insert v (↑x ∩ ↑y))x:Fin k → ℝ⊢ x ∈ insert v ↑x✝ ∩ insert v ↑y ↔ x ∈ insert v (↑x✝ ∩ ↑y) ; aesopAll goals completed! 🐙;
  ·inl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = sht:t = {v}⊢ ∀ x ∈ (convexHull ℝ) ↑s, x = v → v ∈ (convexHull ℝ) (↑s ∩ {v}) contrapose! hvinl.inl.inl.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = sht:t = {v}hv:∃ x ∈ (convexHull ℝ) ↑s, x = v ∧ v ∉ (convexHull ℝ) (↑s ∩ {v})⊢ v ∈ affineSpan ℝ K'.space;
    obtain ⟨ x, hx, rfl, hx' ⟩ := hvinl.inl.inl.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)x:Fin k → ℝhx:x ∈ (convexHull ℝ) ↑shs:s ∈ K'.faces ∨ ∃ x_1 ∈ K'.faces, insert x x_1 = sht:t = {x}hx':x ∉ (convexHull ℝ) (↑s ∩ {x})⊢ x ∈ affineSpan ℝ K'.space;
    refine' face_convexHull_subset_affineSpan K' _ |> fun h => h hxinl.inl.inl.inrk:ℕK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)x:Fin k → ℝhx:x ∈ (convexHull ℝ) ↑shs:s ∈ K'.faces ∨ ∃ x_1 ∈ K'.faces, insert x x_1 = sht:t = {x}hx':x ∉ (convexHull ℝ) (↑s ∩ {x})⊢ s ∈ K'.faces;
    aesopAll goals completed! 🐙;
  ·inl.inr.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spaces:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s = {v}ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = t⊢ v ∈ (convexHull ℝ) ↑t → v ∈ (convexHull ℝ) ({v} ∩ ↑t) contrapose! hvinl.inr.inl.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s = {v}ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = thv:v ∈ (convexHull ℝ) ↑t ∧ v ∉ (convexHull ℝ) ({v} ∩ ↑t)⊢ v ∈ affineSpan ℝ K'.space;
    exact face_convexHull_subset_affineSpan K' ( ht.elim ( fun h => h ) fun ⟨ x, hx, hx' ⟩ => hx' ▸ byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)s:Finset (Fin k → ℝ)t:Finset (Fin k → ℝ)hs:s = {v}ht:t ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = thv:v ∈ (convexHull ℝ) ↑t ∧ v ∉ (convexHull ℝ) ({v} ∩ ↑t)x✝:∃ x ∈ K'.faces, insert v x = tx:Finset (Fin k → ℝ)hx:x ∈ K'.faceshx':insert v x = t⊢ insert v x ∈ K'.faces aesopAll goals completed! 🐙 ) hv.1

/-- The cone with apex `v` over a simplicial complex `K'` (`v` off `affineSpan K'.space`). -/
noncomputable def coneComplex (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ))
    (hv : v ∉ affineSpan ℝ K'.space) :
    SimplicialComplex ℝ (Fin k → ℝ) :=
  SimplicialComplex.ofErase
    (coneFaceSet v K')
    (coneFaceSet_indep v K' hv)
    (coneFaceSet_isLowerSet v K')
    (coneFaceSet_inter v K' hv)

/-
The underlying space of the cone is the convex join of `{v}` with `K'.space`.
-/
lemma coneComplex_space (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ))
    (hv : v ∉ affineSpan ℝ K'.space) (hne : K'.space.Nonempty) :
    (coneComplex v K' hv).space = convexJoin ℝ {v} K'.space := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonempty⊢ (coneComplex v K' hv).space = convexJoin ℝ {v} K'.space
  refine' Set.Subset.antisymm _ _refine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonempty⊢ (coneComplex v K' hv).space ⊆ convexJoin ℝ {v} K'.spacerefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonempty⊢ convexJoin ℝ {v} K'.space ⊆ (coneComplex v K' hv).space;
  ·refine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonempty⊢ (coneComplex v K' hv).space ⊆ convexJoin ℝ {v} K'.space intro x hxrefine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx:x ∈ (coneComplex v K' hv).space⊢ x ∈ convexJoin ℝ {v} K'.space;
    obtain ⟨ s, hs, hx ⟩ := ( coneComplex v K' hv ).mem_space_iff.mp hxrefine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑s⊢ x ∈ convexJoin ℝ {v} K'.space;
    -- Since $s$ is a face of the cone complex, it must be of the form $insert v σ$ for some $σ ∈ K'.faces$ or $σ = ∅$.
    by_cases hs_empty : s = ∅ ∨ s = {v}posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:s = ∅ ∨ s = {v}⊢ x ∈ convexJoin ℝ {v} K'.spacenegk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})⊢ x ∈ convexJoin ℝ {v} K'.space;
    ·posk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:s = ∅ ∨ s = {v}⊢ x ∈ convexJoin ℝ {v} K'.space rcases hs_empty with ( rfl | rfl )pos.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spacehs:∅ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑∅⊢ x ∈ convexJoin ℝ {v} K'.spacepos.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spacehs:{v} ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑{v}⊢ x ∈ convexJoin ℝ {v} K'.space <;>pos.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spacehs:∅ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑∅⊢ x ∈ convexJoin ℝ {v} K'.spacepos.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spacehs:{v} ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑{v}⊢ x ∈ convexJoin ℝ {v} K'.space simp_all +decide [ convexJoin ]pos.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:v ∈ (coneComplex v K' hv).spacehs:{v} ∈ (coneComplex v K' hv).faceshx:x = v⊢ ∃ i ∈ K'.space, v ∈ segment ℝ v i;
      exact ⟨ hne.some, hne.choose_spec, left_mem_segment _ _ _ ⟩All goals completed! 🐙;
    ·negk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})⊢ x ∈ convexJoin ℝ {v} K'.space -- Since $s$ is not empty and not equal to $\{v\}$, it must be of the form $insert v σ$ for some $σ ∈ K'.faces$.
      obtain ⟨σ, hσ⟩ : ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})⊢ ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ
        have := hsk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})this:s ∈ (coneComplex v K' hv).faces⊢ ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ;
        unfold coneComplex at thisk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})this:s ∈ (SimplicialComplex.ofErase (coneFaceSet v K') ⋯ ⋯ ⋯).faces⊢ ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ;
        unfold SimplicialComplex.ofErase at thisk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})this:s ∈ { faces := coneFaceSet v K' \ {∅}, isRelLowerSet_faces := ⋯, indep := ⋯, inter_subset_convexHull := ⋯ }.faces⊢ ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ; simp_all +decide [ coneFaceSet ]k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬s = ∅ ∧ ¬s = {v}this:s ∈ K'.faces ∨ ∃ x ∈ K'.faces, insert v x = s⊢ ∃ σ ∈ K'.faces, s = insert v σ ∨ s = σ ;
        grindAll goals completed! 🐙;
      cases hσ.2neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces ∧ (s = insert v σ ∨ s = σ)h✝:s = insert v σ⊢ x ∈ convexJoin ℝ {v} K'.spaceneg.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces ∧ (s = insert v σ ∨ s = σ)h✝:s = σ⊢ x ∈ convexJoin ℝ {v} K'.space <;>neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces ∧ (s = insert v σ ∨ s = σ)h✝:s = insert v σ⊢ x ∈ convexJoin ℝ {v} K'.spaceneg.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑shs_empty:¬(s = ∅ ∨ s = {v})σ:Finset (Fin k → ℝ)hσ:σ ∈ K'.faces ∧ (s = insert v σ ∨ s = σ)h✝:s = σ⊢ x ∈ convexJoin ℝ {v} K'.space simp_all +decide [ convexJoin_singleton_left ]neg.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑σhs_empty:¬σ = ∅ ∧ ¬σ = {v}hσ:σ ∈ K'.facesh✝:s = σ⊢ ∃ i ∈ K'.space, x ∈ segment ℝ v i;
      ·neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) (insert v ↑σ)hs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ ∃ i ∈ K'.space, x ∈ segment ℝ v i rw [ convexHull_insert ] at hxneg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑σ)hs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ ∃ i ∈ K'.space, x ∈ segment ℝ v ineg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) (insert v ↑σ)hs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ (↑σ).Nonempty;
        ·neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑σ)hs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ ∃ i ∈ K'.space, x ∈ segment ℝ v i simp_all +decide [ convexJoin_singleton_left, segment_eq_image ]neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:∃ i ∈ (convexHull ℝ) ↑σ, ∃ x_1, (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ (1 - x_1) • v + x_1 • i = xhs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ ∃ i ∈ K'.space, ∃ x_1, (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ (1 - x_1) • v + x_1 • i = x;
          exact ⟨ hx.choose, K'.mem_space_iff.mpr ⟨ σ, hσ, hx.choose_spec.1 ⟩, hx.choose_spec.2 ⟩All goals completed! 🐙;
        ·neg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) (insert v ↑σ)hs_empty:¬insert v σ = {v}hσ:σ ∈ K'.facesh✝:s = insert v σ⊢ (↑σ).Nonempty contrapose! hs_emptyneg.inlk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:insert v σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) (insert v ↑σ)hσ:σ ∈ K'.facesh✝:s = insert v σhs_empty:↑σ = ∅⊢ insert v σ = {v}; aesopAll goals completed! 🐙;
      ·neg.inrk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑σhs_empty:¬σ = ∅ ∧ ¬σ = {v}hσ:σ ∈ K'.facesh✝:s = σ⊢ ∃ i ∈ K'.space, x ∈ segment ℝ v i exact ⟨ x, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑σhs_empty:¬σ = ∅ ∧ ¬σ = {v}hσ:σ ∈ K'.facesh✝:s = σ⊢ x ∈ K'.space
          exact Set.mem_iUnion₂.mpr ⟨ σ, hσ, hx ⟩All goals completed! 🐙, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx✝:x ∈ (coneComplex v K' hv).spaces:Finset (Fin k → ℝ)σ:Finset (Fin k → ℝ)hs:σ ∈ (coneComplex v K' hv).faceshx:x ∈ (convexHull ℝ) ↑σhs_empty:¬σ = ∅ ∧ ¬σ = {v}hσ:σ ∈ K'.facesh✝:s = σ⊢ x ∈ segment ℝ v x
          exact right_mem_segment _ _ _All goals completed! 🐙 ⟩;
  ·refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonempty⊢ convexJoin ℝ {v} K'.space ⊆ (coneComplex v K' hv).space intro x hxrefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx:x ∈ convexJoin ℝ {v} K'.space⊢ x ∈ (coneComplex v K' hv).space; simp_all +decide [ convexJoin ]refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝhx:∃ i ∈ K'.space, x ∈ segment ℝ v i⊢ x ∈ (coneComplex v K' hv).space ;
    obtain ⟨ y, hy, hx ⟩ := hxrefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝy:Fin k → ℝhy:y ∈ K'.spacehx:x ∈ segment ℝ v y⊢ x ∈ (coneComplex v K' hv).space; rw [ segment_eq_image ] at hxrefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyx:Fin k → ℝy:Fin k → ℝhy:y ∈ K'.spacehx:x ∈ (fun θ => (1 - θ) • v + θ • y) '' Set.Icc 0 1⊢ x ∈ (coneComplex v K' hv).space; obtain ⟨ t, ht, rfl ⟩ := hxrefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝhy:y ∈ K'.spacet:ℝht:t ∈ Set.Icc 0 1⊢ (fun θ => (1 - θ) • v + θ • y) t ∈ (coneComplex v K' hv).space; simp_all +decide [ SimplicialComplex.mem_space_iff ]refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝhy:∃ s ∈ K'.faces, y ∈ (convexHull ℝ) ↑sht:0 ≤ t ∧ t ≤ 1⊢ ∃ s ∈ (coneComplex v K' hv).faces, (1 - t) • v + t • y ∈ (convexHull ℝ) ↑s ;
    obtain ⟨ s, hs, hy ⟩ := hyrefine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ ∃ s ∈ (coneComplex v K' hv).faces, (1 - t) • v + t • y ∈ (convexHull ℝ) ↑s; use insert v shk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ insert v s ∈ (coneComplex v K' hv).faces ∧ (1 - t) • v + t • y ∈ (convexHull ℝ) ↑(insert v s); simp_all +decide [ coneComplex ]hk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ insert v s ∈ coneFaceSet v K' ∧ (1 - t) • v + t • y ∈ (convexHull ℝ) (insert v ↑s) ;
    refine' ⟨ _, _ ⟩h.refine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ insert v s ∈ coneFaceSet v K'h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (1 - t) • v + t • y ∈ (convexHull ℝ) (insert v ↑s);
    ·h.refine'_1k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ insert v s ∈ coneFaceSet v K' exact Set.mem_union_left _ ( Set.mem_union_left _ ( Set.mem_union_right _ ( Set.mem_image_of_mem _ hs ) ) )All goals completed! 🐙;
    ·h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (1 - t) • v + t • y ∈ (convexHull ℝ) (insert v ↑s) rw [ convexHull_insert ]h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (1 - t) • v + t • y ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑s)h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (↑s).Nonempty <;>h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (1 - t) • v + t • y ∈ convexJoin ℝ {v} ((convexHull ℝ) ↑s)h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ (↑s).Nonempty norm_num [ hy ]h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ s.Nonempty;
      ·h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ ∃ i ∈ (convexHull ℝ) ↑s, (1 - t) • v + t • y ∈ segment ℝ v i exact ⟨ y, hy, ⟨ 1 - t, t, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ 0 ≤ 1 - t linarithAll goals completed! 🐙, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ 0 ≤ t linarithAll goals completed! 🐙, byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ 1 - t + t = 1 ∧ (1 - t) • v + t • y = (1 - t) • v + t • y simp +decide [ add_comm ]All goals completed! 🐙 ⟩ ⟩;
      ·h.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑s⊢ s.Nonempty contrapose! hvh.refine'_2k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hne:K'.space.Nonemptyy:Fin k → ℝt:ℝht:0 ≤ t ∧ t ≤ 1s:Finset (Fin k → ℝ)hs:s ∈ K'.faceshy:y ∈ (convexHull ℝ) ↑shv:s = ∅⊢ v ∈ affineSpan ℝ K'.space; aesopAll goals completed! 🐙;

/-
If `K'.faces` is finite, so are the cone's faces.
-/
lemma coneComplex_faces_finite (v : Fin k → ℝ) (K' : SimplicialComplex ℝ (Fin k → ℝ))
    (hv : v ∉ affineSpan ℝ K'.space) (hfin : K'.faces.Finite) :
    (coneComplex v K' hv).faces.Finite := byk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehfin:K'.faces.Finite⊢ (coneComplex v K' hv).faces.Finite
  refine' Set.Finite.subset ( hfin.union ( Set.Finite.image ( fun s => insert v s ) hfin ) |> Set.Finite.union <| Set.finite_singleton { v } |> Set.Finite.union <| Set.finite_singleton ∅ ) _k:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehfin:K'.faces.Finite⊢ (coneComplex v K' hv).faces ⊆ K'.faces ∪ (fun s => insert v s) '' K'.faces ∪ ({{v}} ∪ {∅});
  intro s hsk:ℕv:Fin k → ℝK':SimplicialComplex ℝ (Fin k → ℝ)hv:v ∉ affineSpan ℝ K'.spacehfin:K'.faces.Finites:Finset (Fin k → ℝ)hs:s ∈ (coneComplex v K' hv).faces⊢ s ∈ K'.faces ∪ (fun s => insert v s) '' K'.faces ∪ ({{v}} ∪ {∅}); simp_all +decide [ coneComplex, coneFaceSet ]All goals completed! 🐙 ;

end FamiliesOfMapsB01
end Submission