awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
x : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)
⊢ Eq (α := Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ :
                    Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                  (Hom.mk
                    { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ :
                      Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
                op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))

Tactic:
exact (II.map'_map' _ _ _).symm

Premises used: SimplexCategory.II.map'_map', Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
a :
  ∀ (x : Fin ((unop (II ^⦋n + 1⦌)).len + 1)),
    Eq (α := Fin ((unop (II ^⦋n⦌)).len + 1))
      ((Hom.toOrderHom (II.δ i).unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
        Fin ((unop (II ^⦋n⦌)).len + 1))
      ((Hom.toOrderHom (σ i).op.unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
        Fin ((unop (II ^⦋n⦌)).len + 1))
⊢ (II.δ i).unop = (σ i).op.unop

Tactic:
ext : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin ((unop (II ^⦋n + 1⦌)).len + 1)
⊢ Eq (α := Fin ((unop (II ^⦋n⦌)).len + 1))
    ((Hom.toOrderHom (II.δ i).unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n⦌)).len + 1))
    ((Hom.toOrderHom (σ i).op.unop : (a : Fin ((unop (II ^⦋n + 1⦌)).len + 1)) → Fin ((unop (II ^⦋n⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n⦌)).len + 1))

Tactic:
apply II.map'_succAboveOrderEmb

Premises used: SimplexCategory.II.map'_succAboveOrderEmb
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 1)
a :
  ∀ (x : Fin ((unop (II ^⦋n⦌)).len + 1)),
    Eq (α := Fin ((unop (II ^⦋n + 1⦌)).len + 1))
      ((Hom.toOrderHom (II.σ i).unop : (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1)) x :
        Fin ((unop (II ^⦋n + 1⦌)).len + 1))
      ((Hom.toOrderHom (δ i.succ.castSucc).op.unop :
            (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1))
          x :
        Fin ((unop (II ^⦋n + 1⦌)).len + 1))
⊢ (II.σ i).unop = (δ i.succ.castSucc).op.unop

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 1)
x : Fin ((unop (II ^⦋n⦌)).len + 1)
⊢ Eq (α := Fin ((unop (II ^⦋n + 1⦌)).len + 1))
    ((Hom.toOrderHom (II.σ i).unop : (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1)) x :
      Fin ((unop (II ^⦋n + 1⦌)).len + 1))
    ((Hom.toOrderHom (δ i.succ.castSucc).op.unop :
          (a : Fin ((unop (II ^⦋n⦌)).len + 1)) → Fin ((unop (II ^⦋n + 1⦌)).len + 1))
        x :
      Fin ((unop (II ^⦋n + 1⦌)).len + 1))

Tactic:
apply II.map'_predAbove

Premises used: SimplexCategory.II.map'_predAbove
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X Y : SimplicialObject.{v, u_1} C
f : X ⟶ Y
n : SimplexCategoryᵒᵖ
⊢ NatTrans.app (CategoryTheory.Functor.map opFunctor f) n = Iso.hom opObjIso ≫ f.app n ≫ Iso.inv opObjIso

Tactic:
simp [opFunctor, opObjIso]

Premises used: SimplicialObject.opObjIso, SimplicialObject.opFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X : SimplicialObject.{v, u_1} C
n m : SimplexCategoryᵒᵖ
f : n ⟶ m
⊢ (Functor.obj opFunctor X).map f = Iso.hom opObjIso ≫ X.map (SimplexCategory.rev.map f.unop).op ≫ Iso.inv opObjIso

Tactic:
simp [opFunctor, opObjIso]

Premises used: SimplicialObject.opObjIso, SimplicialObject.opFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X : SimplicialObject.{v, u_1} C
n : ℕ
i : Fin (n + 2)
⊢ (Functor.obj opFunctor X).δ i = Iso.hom opObjIso ≫ X.δ i.rev ≫ Iso.inv opObjIso

Tactic:
simp [SimplicialObject.δ]

Premises used: CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X : SimplicialObject.{v, u_1} C
n : ℕ
i : Fin (n + 1)
⊢ (Functor.obj opFunctor X).σ i = Iso.hom opObjIso ≫ X.σ i.rev ≫ Iso.inv opObjIso

Tactic:
simp [SimplicialObject.σ]

Premises used: CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X : SimplicialObject.{v, u_1} C
n : SimplexCategoryᵒᵖ
⊢ (NatTrans.app (Iso.hom opFunctorCompOpFunctorIso) X).app n = Iso.hom opObjIso ≫ Iso.hom opObjIso

Tactic:
simp [opFunctorCompOpFunctorIso, opObjIso, opFunctor]

Premises used: SimplicialObject.opFunctorCompOpFunctorIso, SimplicialObject.opObjIso, SimplicialObject.opFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Op
Goal:
C : Type u_1
inst : Category.{v, u_1} C
X : SimplicialObject.{v, u_1} C
n : SimplexCategoryᵒᵖ
⊢ (NatTrans.app (Iso.inv opFunctorCompOpFunctorIso) X).app n = Iso.inv opObjIso ≫ Iso.inv opObjIso

Tactic:
simp [opFunctorCompOpFunctorIso, opObjIso, opFunctor]

Premises used: SimplicialObject.opFunctorCompOpFunctorIso, SimplicialObject.opObjIso, SimplicialObject.opFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Epi A.e

Tactic:
A.2.2

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.e, Sigma.snd, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A =
    Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
      (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
      (Subtype.mk (p :=
        fun (α : unop Δ ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ↦ Epi α)
        A.e ⋯)

Tactic:
rfl

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet, CategoryTheory.SimplicialObject.Splitting.IndexSet.e, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ :
  A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
rw rw₁ :
  unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) =
    unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
⊢ unop (A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) =
    unop (A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))

Tactic:
rw [h₁]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ :
  A₁.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
rcases :
  ∀ (Δ₁ : SimplexCategoryᵒᵖ) (α₁ : unop Δ ⟶ unop Δ₁) (hα₁ : Epi α₁)
    (h₁ :
      Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
        A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
    (h₂ :
      e
            (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
              (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
          eqToHom ⋯ =
        A₂.e),
    Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁) =
      A₂
⊢ A₁ = A₂

Tactic:
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ :
  Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
    A₂.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
h₂ :
  e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
      eqToHom ⋯ =
    A₂.e
rcases :
  ∀ (Δ₂ : SimplexCategoryᵒᵖ) (α₂ : unop Δ ⟶ unop Δ₂) (hα₂ : Epi α₂)
    (h₁ :
      Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) =
        Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂)))
    (h₂ :
      e
            (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
              (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)) ≫
          eqToHom ⋯ =
        e
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))),
    Eq (α := IndexSet Δ)
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))
⊢ Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁) =
    A₂

Tactic:
rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ :
  Eq (α :=
    unop Δ ⟶
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))))
    (CategoryStruct.comp (Y :=
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
      (e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
      (eqToHom ⋯))
    (e
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂)))
subst :
  ∀ (α₂ : unop Δ ⟶ unop Δ₁) (hα₂ : Epi α₂)
    (h₂ :
      Eq (α :=
        unop Δ ⟶
          unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
              (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
                (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))))
        (CategoryStruct.comp (Y :=
          unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
              (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
                (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
          (e
            (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
              (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
          (eqToHom ⋯))
        (e
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂)))),
    Eq (α := IndexSet Δ)
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))
⊢ Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₂
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₂) ↦ Epi α) α₂ hα₂))

Tactic:
subst h₁
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ :
  Eq (α :=
    unop Δ ⟶
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))))
    (CategoryStruct.comp (Y :=
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
            (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))))
      (e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁)))
      (eqToHom ⋯))
    (e
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
        (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂)))
⊢ α₁ = α₂

Tactic:
simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
α₂ : unop Δ ⟶ unop Δ₁
hα₂ : Epi α₂
h₂ : α₁ = α₂
⊢ Eq (α := IndexSet Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₁ hα₁))
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) Δ₁
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop Δ₁) ↦ Epi α) α₂ hα₂))

Tactic:
simp only [h₂]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Eq (α := (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1)))
    ((fun (A : IndexSet Δ) ↦
        (Sigma.mk (β := fun (k : Fin ((unop Δ).len + 1)) ↦ Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))
            ⟨(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len, ⋯⟩
            (⇑(Hom.toOrderHom A.e) : (a : Fin ((unop Δ).len + 1)) → Fin ((unop A.fst).len + 1)) :
          (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))
    ((fun (A : IndexSet Δ) ↦
        (Sigma.mk (β := fun (k : Fin ((unop Δ).len + 1)) ↦ Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))
            ⟨(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len, ⋯⟩
            (⇑(Hom.toOrderHom A.e) : (a : Fin ((unop Δ).len + 1)) → Fin ((unop A.fst).len + 1)) :
          (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))
⊢ Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))

Tactic:
simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁

Premises used: Fin.mk.injEq, Opposite.unop_op, Sigma.mk.inj_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
len : Δ₁.len = Δ₂.len
⊢ Δ₁ = Δ₂

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
⊢ Δ₁.len = Δ₂.len

Tactic:
simpa only [Fin.mk_eq_mk] using h₁.1

Premises used: Fin.mk_eq_mk, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
⊢ Δ₁ = Δ₂

Tactic:
have h₂ : Δ₁ = Δ₂ := by
        ext1
        simpa only [Fin.mk_eq_mk] using h₁.1
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
h₂ : Δ₁ = Δ₂
subst :
  ∀ (α₂ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α })
    (h₁ :
      Δ₁.len = Δ₁.len ∧
        HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
          (⇑(Hom.toOrderHom
                (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
            (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
          (β := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
          (⇑(Hom.toOrderHom
                (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
            (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))),
    Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂)

Tactic:
subst h₂
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ α₂ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
h₁ :
  Δ₁.len = Δ₁.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)

Tactic:
ext _ _ rfl ?_

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.ext, rfl