awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) 3 multicofork_π_three._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) 3 multicofork_π_three._proof_1))
    (Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ 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₃
rw : horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀
⊢ ι₀ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₀

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 0).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- 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 (α := ℕ) 2 1 + 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₃
⊢ horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀

Tactic:
exact (horn.isColimit 1).fac _ (.right ⟨0, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- 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₃
rw : horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 2) ≫ f₂
⊢ ι₂ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₂

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 2).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- 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 (α := ℕ) 2 1 + 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₃
⊢ horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 2) ≫ f₂

Tactic:
exact (horn.isColimit 1).fac _ (.right ⟨2, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- 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₃
rw : horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃
⊢ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- 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 (α := ℕ) 2 1 + 1))) {1}ᶜ 3

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₃
⊢ horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃

Tactic:
exact (horn.isColimit 1).fac _ (.right ⟨3, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- 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₃
⊢ ι₀ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₀ ∧ ι₂ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₂ ∧ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃

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

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

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

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

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{2}ᶜ : 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))) {2}ᶜ 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))) {2}ᶜ 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.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {2}ᶜ 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{2}ᶜ : 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))) {2}ᶜ x) 1 multicofork_π_one._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))) {2}ᶜ x) 1 multicofork_π_one._proof_1))
    (Iso.inv (stdSimplex.faceSingletonComplIso 1) ≫ 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.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 3 1))) {2}ᶜ 3

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{2}ᶜ : 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))) {2}ᶜ x) 3 multicofork_π_three._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))) {2}ᶜ x) 3 multicofork_π_three._proof_1))
    (Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ 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.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
rw : horn.faceι 2 0 ι₀._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 0).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1 + 1))) {2}ᶜ 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 0 ι₀._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀

Tactic:
exact (horn.isColimit 2).fac _ (.right ⟨0, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
rw : horn.faceι 2 1 ι₁._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 1) ≫ f₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 1).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1 + 1))) {2}ᶜ 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 1 ι₁._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 1) ≫ f₁

Tactic:
exact (horn.isColimit 2).fac _ (.right ⟨1, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
rw : horn.faceι 2 3 ι₃._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃
⊢ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Premises used: CategoryTheory.Category.assoc, SSet.horn.faceSingletonComplIso_inv_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1 + 1))) {2}ᶜ 3

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 3 ι₃._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃

Tactic:
exact (horn.isColimit 2).fac _ (.right ⟨3, by simp⟩)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingMultispan.right, Subtype.mk, SSet.horn.isColimit, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀ ∧ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁ ∧ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
⊢ φ ≫ s.map = const x

Tactic:
(Subcomplex.lift φ ?_) ≫= s.comm

Premises used: CategoryTheory.NatTrans.vcomp, SSet.const, CategoryTheory.Functor.comp, TypeCat.Fun.comp, CategoryTheory.Subfunctor.toFunctor, SSet.RelativeMorphism.comm, SSet.Subcomplex.lift, CategoryTheory.Subfunctor.lift, CategoryTheory.whisker_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
refine : Subcomplex.range φ ≤ ∂Δ[n]
⊢ φ ≫ s.map = const x

Tactic:
refine (Subcomplex.lift φ ?_) ≫= s.comm

Premises used: SSet.RelativeMorphism.comm, SSet.Subcomplex.lift
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
rw : Subcomplex.range φ ≠ ⊤
⊢ Subcomplex.range φ ≤ ∂Δ[n]

Tactic:
rw [stdSimplex.le_boundary_iff]

Premises used: SSet.stdSimplex.le_boundary_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
rw : IsIso.{u, u + 1} (X := Subcomplex.toSSet (X := Δ[n]) ⊤) (Subcomplex.ι ⊤)
⊢ IsIso (Subcomplex.range φ).ι

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso.{u, u + 1} (X := Subcomplex.toSSet (X := Δ[n]) ⊤) (Subcomplex.ι ⊤)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso (Subcomplex.range φ).ι

Tactic:
have : IsIso (Subcomplex.range φ).ι := by rw [h]; infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
this : IsIso (Subcomplex.range φ).ι
⊢ False

Tactic:
stdSimplex.not_hasDimensionLT n
    ((hasDimensionLT_iff_of_iso (asIso (Subcomplex.range φ).ι) n).mp inferInstance)

Premises used: SSet.Subcomplex.range, SSet.stdSimplex.not_hasDimensionLT, inferInstance, SSet.Subcomplex.ι, Iff.mp, SSet.hasDimensionLT_iff_of_iso, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
this : IsIso (Subcomplex.range φ).ι
⊢ False

Tactic:
exact stdSimplex.not_hasDimensionLT n
    ((hasDimensionLT_iff_of_iso (asIso (Subcomplex.range φ).ι) n).mp inferInstance)

Premises used: SSet.Subcomplex.range, SSet.stdSimplex.not_hasDimensionLT, inferInstance, SSet.Subcomplex.ι, Iff.mp, SSet.hasDimensionLT_iff_of_iso, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex (n + 1) x
i : Fin (n + 2)
⊢ stdSimplex.δ i ≫ f.map = const x

Tactic:
comp_map_eq_const _ _

Premises used: SSet.PtSimplex.comp_map_eq_const
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
rw rw₁ : f.map = f.map
⊢ stdSimplex.δ i.castSucc ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
rw [CosimplicialObject.δ_comp_σ_self_assoc]

Premises used: CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
rw rw₁ : f.map = f.map
⊢ stdSimplex.δ i.succ ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
rw [CosimplicialObject.δ_comp_σ_succ_assoc]

Premises used: CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : j < i.castSucc
⊢ i ≠ 0

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : j < i.castSucc
obtain : ∀ (i : Fin n) (hj : j < i.succ.castSucc), stdSimplex.δ j ≫ stdSimplex.σ i.succ ≫ f.map = const x
⊢ stdSimplex.δ j ≫ stdSimplex.σ i ≫ f.map = const x

Tactic:
obtain ⟨i, rfl⟩ := i.eq_succ_of_ne_zero (by aesop)

Premises used: Fin.eq_succ_of_ne_zero, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : j < i.succ.castSucc
⊢ j ≠ Fin.last (n + 1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : j < i.succ.castSucc
obtain :
  ∀ (j : Fin (n + 1)) (hj : j.castSucc < i.succ.castSucc),
    stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
⊢ stdSimplex.δ j ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (by grind)

Premises used: Fin.eq_castSucc_of_ne_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : j.castSucc < i.succ.castSucc
zero :
  ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : j.castSucc < i.succ.castSucc),
    stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
succ :
  ∀ (n : ℕ) (f : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) (j : Fin (n + 1 + 1)) (hj : j.castSucc < i.succ.castSucc),
    stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
f : X.PtSimplex 0 x
i : Fin 0
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
fin_cases i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ j ≤ i.castSucc

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
succ₁ : stdSimplex.σ i ≫ const x = const x
succ₂ succ₃ : Eq (α := Δ[n + 1] ⟶ X) (const x) (const x)
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
rw [stdSimplex.δ_comp_σ_of_le_assoc (by grind), δ_map, comp_const]

Premises used: SSet.stdSimplex, SSet.comp_const, SSet.PtSimplex.δ_map, CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : i.succ < j
⊢ i ≠ Fin.last n

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : i.succ < j
obtain : ∀ (i : Fin n) (hj : i.castSucc.succ < j), stdSimplex.δ j ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
⊢ stdSimplex.δ j ≫ stdSimplex.σ i ≫ f.map = const x

Tactic:
obtain ⟨i, rfl⟩ := i.eq_castSucc_of_ne_last (by grind)

Premises used: Fin.eq_castSucc_of_ne_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : i.castSucc.succ < j
⊢ j ≠ 0

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : i.castSucc.succ < j
obtain :
  ∀ (j : Fin (n + 1)) (hj : i.castSucc.succ < j.succ), stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
⊢ stdSimplex.δ j ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (by aesop)

Premises used: Fin.eq_succ_of_ne_zero, rfl