awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
apply : Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]

Tactic:
apply le_antisymm (Subfunctor.equalizer_le σ₁ σ₂)

Premises used: CategoryTheory.Subfunctor.equalizer_le, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
simp :
  ∀ (a : Fin (n + 1 + 1)) (b : ¬a = i),
    Membership.mem (α := Δ[n + 1] _⦋n⦌) (γ := Set (Δ[n + 1] _⦋n⦌)) ((Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌))
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ a) : Δ[n + 1] _⦋n⦌)
⊢ Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂

Tactic:
simp only [horn_eq_iSup, iSup_le_iff,
    Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
    ← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]

Premises used: Subtype.forall, SSet.Subcomplex.ofSimplex_le_iff, Set.mem_singleton_iff, SSet.horn_eq_iSup, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, iSup_le_iff, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
j : Fin (n + 1 + 1)
hj : ¬j = i
⊢ Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Subfunctor.toFunctor Λ[n + 1, i] _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
        (face i j hj) :
      (fun (X : Type u) ↦ X) (S _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Subfunctor.toFunctor Λ[n + 1, i] _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
        (face i j hj) :
      (fun (X : Type u) ↦ X) (S _⦋n⦌))

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    Eq (α := (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₁.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₂.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1, i].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (S _⦋n⦌))
          (face i j h) :
        (fun (X : Type u) ↦ X) (S _⦋n⦌))
j : Fin (n + 1 + 1)
hj : ¬j = i
⊢ Membership.mem (α := Δ[n + 1] _⦋n⦌) (γ := Set (Δ[n + 1] _⦋n⦌)) ((Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌))
    ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.δ j) : Δ[n + 1] _⦋n⦌)

Tactic:
exact (Subfunctor.mem_equalizer_iff σ₁ σ₂ (face i j hj)).2 (by apply h)

Premises used: Iff.mpr, CategoryTheory.Subfunctor.mem_equalizer_iff, SSet.horn.face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 1)
hij : j ≠ i
⊢ faceι i j hij ≫ Λ[n, i].ι = Subcomplex.ι (stdSimplex.face {j}ᶜ)

Tactic:
simp [faceι]

Premises used: SSet.horn.faceι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
      ((Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij)) =
    face i j hij
rw₁ rw₂ : face i j hij = face i j hij
⊢ (yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌) (ι i j hij) = face i j hij

Tactic:
rw [ι, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, SSet.horn.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet) (face i j hij) ≫ Λ[n + 1, i].ι =
    stdSimplex.δ j
rw₁ :
  (Equiv.symm yonedaEquiv : (a : Λ[n + 1, i].toSSet _⦋n⦌) → Δ[n] ⟶ Λ[n + 1, i].toSSet)
        ((yonedaEquiv : (a : Δ[n] ⟶ Λ[n + 1, i].toSSet) → Λ[n + 1, i].toSSet _⦋n⦌)
            (Subfunctor.lift (stdSimplex.δ j) ⋯) :
          Λ[n + 1, i].toSSet _⦋n⦌) ≫
      Λ[n + 1, i].ι =
    stdSimplex.δ j
rw₂ : Subfunctor.lift (stdSimplex.δ j) ⋯ ≫ Λ[n + 1, i].ι = stdSimplex.δ j
rw₃ rw₄ : stdSimplex.δ j = stdSimplex.δ j
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]

Premises used: Equiv.symm_apply_apply, SSet.horn.ι, CategoryTheory.Subfunctor.lift_ι, SSet.horn.face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
rw : ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} j).hom, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 0] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}) Λ[2, 0]

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0]

Tactic:
exact face_le_horn (2 : Fin 3) 0 (by simp)

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]

Tactic:
exact face_le_horn (1 : Fin 3) 0 (by simp)

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  ∀ (i : (↑{0}ᶜ : Type)),
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
      (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 0] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
rw [horn_eq_iSup, iSup_le_iff]

Premises used: SSet.horn_eq_iSup, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
i : (↑{0}ᶜ : Type)
a :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
a₁ :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
le_sup_right

Premises used: Set.Mem, List.elem, setOf, Fin.ofNat, le_sup_right, Multiset.ofList, List.erase, Multiset.sub, List.diff, Multiset.ndinsert, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem, List.elem, setOf, Fin.ofNat, Multiset.ofList, List.erase, Multiset.sub, List.diff, Multiset.ndinsert, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊓ stdSimplex.face {0, 2}) (stdSimplex.face {0})

Tactic:
simp [stdSimplex.face_inter_face]

Premises used: SSet.stdSimplex.face_inter_face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 1 2)) 2 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 1 2)) 1 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
comminl :
  Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))
comminr :
  Iso.hom (stdSimplex.facePairIso 0 2 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))
⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

Tactic:
fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.facePairIso 0 2 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 1] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 2 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1]

Tactic:
exact face_le_horn (2 : Fin 3) 1 (by simp)

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]

Tactic:
exact face_le_horn (0 : Fin 3) 1 (by simp)

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  ∀ (i : (↑{1}ᶜ : Type)),
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
      (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 1] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
rw [horn_eq_iSup, iSup_le_iff]

Premises used: SSet.horn_eq_iSup, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
i : (↑{1}ᶜ : Type)
a :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
a₁ :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
le_sup_right

Premises used: Set.Mem, List.elem, setOf, Fin.ofNat, le_sup_right, Multiset.ofList, List.erase, Multiset.sub, List.diff, Multiset.ndinsert, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem, List.elem, setOf, Fin.ofNat, Multiset.ofList, List.erase, Multiset.sub, List.diff, Multiset.ndinsert, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊓ stdSimplex.face {1, 2}) (stdSimplex.face {1})

Tactic:
simp [stdSimplex.face_inter_face]

Premises used: SSet.stdSimplex.face_inter_face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 1 2)) 2 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 1 2)) 0 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)
comminl :
  Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))
comminr :
  Iso.hom (stdSimplex.facePairIso 1 2 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₁₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂

Tactic:
apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Iso.hom (stdSimplex.facePairIso 1 2 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₁₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 2] (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2]
a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 1 2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2]

Tactic:
exact face_le_horn (1 : Fin 3) 2 (by simp)

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) 0 2

Tactic:
simp