awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]

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

Premises used: SSet.face_le_horn, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
a :
  ∀ (i : (↑{2}ᶜ : Type)),
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
      (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 2] (stdSimplex.face {0, 2} ⊔ 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 : (↑{2}ᶜ : 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ 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, 2} ⊓ stdSimplex.face {1, 2}) (stdSimplex.face {2})

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)) 1 2

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

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

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 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)

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

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, 2]))

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, 2]))

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
i : Fin (n + 1)
rw rw₁ :
  Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (⨆ (i_1 : (↑{i}ᶜ : Type)), stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ)
    (⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ)
⊢ ⨆ (i_1 : (↑{i}ᶜ : Type)), stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ = Λ[n, i]

Tactic:
rw [horn_eq_iSup]

Premises used: SSet.horn_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
i : Fin (n + 1)
j k : (↑{i}ᶜ : Type)
rw :
  Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
    (stdSimplex.face ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ))
⊢ Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
    (stdSimplex.face {(↑j : Fin (n + 1))}ᶜ ⊓ stdSimplex.face {(↑k : Fin (n + 1))}ᶜ)

Tactic:
rw [stdSimplex.face_inter_face]

Premises used: SSet.stdSimplex.face_inter_face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
i : Fin (n + 1)
j k : (↑{i}ᶜ : Type)
e_S :
  Eq (α := Finset (Fin (n + 1))) {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ
    ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ)
⊢ Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
    (stdSimplex.face ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
i : Fin (n + 1)
j k : (↑{i}ᶜ : Type)
⊢ Eq (α := Finset (Fin (n + 1))) {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ
    ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f g : Λ[n + 1, i].toSSet ⟶ X
h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), ι i j hj ≫ f = ι i j hj ≫ g
⊢ f = g

Tactic:
Multicofork.IsColimit.hom_ext (isColimit i) (fun ⟨j, hj⟩ ↦ ?_)

Premises used: CategoryTheory.Limits.Multicofork.IsColimit.hom_ext, Set.Mem, CategoryTheory.Limits.Multicofork.map, CategoryTheory.Subfunctor.toFunctor, SSet.horn.isColimit, _private.0.SSet.horn.hom_ext'.match_1, CompleteLattice.MulticoequalizerDiagram.multicofork, SSet.horn.multicoequalizerDiagram, CategoryTheory.CategoryStruct.comp, SSet.Subcomplex.toSSetFunctor, CategoryTheory.Limits.Multicofork.toLinearOrder, Eq, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f g : Λ[n + 1, i].toSSet ⟶ X
h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), ι i j hj ≫ f = ι i j hj ≫ g
refine :
  ∀ (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) (j : Fin (n + 1 + 1))
    (hj : Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ j),
    Eq (α :=
      MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{i}ᶜ : Type))
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ⟶
        X)
      (Multicofork.π
          (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
        f)
      (Multicofork.π
          (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
        g)
⊢ f = g

Tactic:
refine Multicofork.IsColimit.hom_ext (isColimit i) (fun ⟨j, hj⟩ ↦ ?_)

Premises used: CategoryTheory.Limits.Multicofork.IsColimit.hom_ext, CategoryTheory.Limits.Multicofork.map, SSet.horn.isColimit, _private.0.SSet.horn.hom_ext'.match_1, CompleteLattice.MulticoequalizerDiagram.multicofork, SSet.horn.multicoequalizerDiagram, CategoryTheory.CategoryStruct.comp, SSet.Subcomplex.toSSetFunctor, CategoryTheory.Limits.Multicofork.toLinearOrder, Eq, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f g : Λ[n + 1, i].toSSet ⟶ X
h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), ι i j hj ≫ f = ι i j hj ≫ g
x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R
j : Fin (n + 1 + 1)
hj : Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ j
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{i}ᶜ : Type))
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ⟶
      X)
    (Multicofork.π
        (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
      f)
    (Multicofork.π
        (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
      g)

Tactic:
simpa only [faceSingletonComplIso_inv_ι_assoc] using
    (stdSimplex.faceSingletonComplIso j).inv ≫= h j hj

Premises used: SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.stdSimplex.faceSingletonComplIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
i : Fin 2
f : (j : Fin 2) → j ≠ i → (Δ[0] ⟶ X)
⊢ horn.IsCompatible f ↔ True

Tactic:
Iff.rfl

Premises used: Iff.rfl, SSet.horn.IsCompatible
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 3)
f : (j : Fin (n + 3)) → j ≠ i → (Δ[n + 1] ⟶ X)
⊢ horn.IsCompatible f ↔
    ∀ (j k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
      stdSimplex.δ (k.pred ⋯) ≫ f j hj = stdSimplex.δ (j.castPred ⋯) ≫ f k hk

Tactic:
Iff.rfl

Premises used: Iff.rfl, SSet.horn.IsCompatible
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
g : Λ[n + 1, i].toSSet ⟶ X
zero :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 2)} (g : Λ[HAdd.hAdd (α := ℕ) 0 1, i].toSSet ⟶ X),
    horn.IsCompatible.{u} (n := 0) (X := X) (i := i) fun (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
succ :
  ∀ (n : ℕ) {i : Fin (n + 1 + 2)} (g : Λ[n + 1 + 1, i].toSSet ⟶ X),
    horn.IsCompatible.{u} (n := n + 1) (X := X) (i := i) fun (j : Fin (n + 1 + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
⊢ horn.IsCompatible.{u} (n := n) (X := X) (i := i) fun (j : Fin (n + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
i : Fin (HAdd.hAdd (α := ℕ) 0 2)
g : Λ[HAdd.hAdd (α := ℕ) 0 1, i].toSSet ⟶ X
⊢ horn.IsCompatible.{u} (n := 0) (X := X) (i := i) fun (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
succ :
  ∀ (j k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
    (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g
⊢ horn.IsCompatible.{u} (n := n + 1) (X := X) (i := i) fun (j : Fin (n + 1 + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g

Tactic:
simp only [isCompatible_iff, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, SSet.horn.isCompatible_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
succ : stdSimplex.δ (k.pred ⋯) ≫ ι i j hj = stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk
⊢ (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
succ :
  ∀ (j : Fin (n + 2)) (hj : j.castSucc ≠ i) (hjk : j.castSucc < k),
    stdSimplex.δ (k.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k hk
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j hj = stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk

Tactic:
obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hjk)

Premises used: Fin.eq_castSucc_of_ne_last, Fin.ne_last_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
k : Fin (n + 3)
hk : k ≠ i
j : Fin (n + 2)
hj : j.castSucc ≠ i
hjk : j.castSucc < k
succ :
  ∀ (k : Fin (n + 2)) (hk : k.succ ≠ i) (hjk : j.castSucc < k.succ),
    stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k hk

Tactic:
obtain ⟨k, rfl⟩ := k.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hjk)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ j ≤ k

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₃ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₄ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
succ₅ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
succ₆ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ j ≫ stdSimplex.δ k.succ
succ₇ succ₈ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ k ≫ stdSimplex.δ j.castSucc
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk

Tactic:
rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]

Premises used: Iff.mpr, CategoryTheory.Category.assoc, Fin.ext_iff, Fin.castPred_castSucc, CategoryTheory.CosimplicialObject.δ_comp_δ, Iff.not, CategoryTheory.cancel_mono, Fin.pred_succ, SSet.stdSimplex, Fin.castSucc_lt_last, SSet.Subcomplex.ι, SSet.horn.ι_ι, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 3)
f : (j : Fin (n + 3)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ f j hj = stdSimplex.δ (j.castPred ⋯) ≫ f k hk

Tactic:
hf j k hj hk hjk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ a
b : Fin (n + 1 + 1 + 1)
hb : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ b
hab : a < b
⊢ ¬a = i

Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at ha hb

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ a
b : Fin (n + 1 + 1 + 1)
hb : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ b
hab : a < b
ha₁ : ¬a = i
⊢ ¬b = i

Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at ha hb

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
rw :
  (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj
⊢ ι i j hj ≫ (isColimit i).desc hf.multicofork = f j hj

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso j).inv]

Premises used: SSet.stdSimplex.faceSingletonComplIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj

Tactic:
simpa using (horn.isColimit.{u} i).fac hf.multicofork (.right ⟨j, hj⟩)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ hf.desc = f j hj

Tactic:
hf.exists_desc.choose_spec j hj

Premises used: Exists.choose_spec, SSet.horn.IsCompatible.exists_desc, SSet.horn.IsCompatible.desc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
⊢ Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 2)) 0 1

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

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{1}ᶜ : Type))
        (MultispanIndex.map (MultispanIndex.toLinearOrder (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯))
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 3 1)) ↦
          Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ x) 0 multicofork_π_zero._proof_1) ⟶
      (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt)
    ((multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π
      (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 3 1)) ↦
        Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ x) 0 multicofork_π_zero._proof_1))
    (Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀)

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Limits.Multicofork.π, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ 2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{1}ᶜ : Type))
        (MultispanIndex.map (MultispanIndex.toLinearOrder (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯))
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 3 1)) ↦
          Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ x) 2 multicofork_π_two._proof_1) ⟶
      (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt)
    ((multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π
      (Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 3 1)) ↦
        Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ x) 2 multicofork_π_two._proof_1))
    (Iso.inv (stdSimplex.faceSingletonComplIso 2) ≫ f₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Limits.Multicofork.π, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {1}ᶜ 3

Tactic:
simp