[GOAL]
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
⊢ A₁.fst.unop = A₂.fst.unop
[PROOFSTEP]
rw [h₁]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : e A₁ ≫ eqToHom (_ : A₁.fst.unop = A₂.fst.unop) = e A₂
⊢ A₁ = A₂
[PROOFSTEP]
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
h₁ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst = A₂.fst
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom (_ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop = A₂.fst.unop) =
    e A₂
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = A₂
[PROOFSTEP]
rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : Δ.unop ⟶ Δ₂.unop
hα₂ : Epi α₂
h₁ : { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only at h₁ 
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : Δ.unop ⟶ Δ₂.unop
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₂, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₂, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
subst h₁
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
α₂ : Δ.unop ⟶ Δ₁.unop
hα₂ : Epi α₂
h₂ :
  e { fst := Δ₁, snd := { val := α₁, property := hα₁ } } ≫
      eqToHom
        (_ :
          { fst := Δ₁, snd := { val := α₁, property := hα₁ } }.fst.unop =
            { fst := Δ₁, snd := { val := α₂, property := hα₂ } }.fst.unop) =
    e { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂ 
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.913, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : Δ.unop ⟶ Δ₁.unop
hα₁ : Epi α₁
α₂ : Δ.unop ⟶ Δ₁.unop
hα₂ : Epi α₂
h₂ : α₁ = α₂
⊢ { fst := Δ₁, snd := { val := α₁, property := hα₁ } } = { fst := Δ₁, snd := { val := α₂, property := hα₂ } }
[PROOFSTEP]
simp only [h₂]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Function.Injective fun A =>
    { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
      snd := ↑(Hom.toOrderHom (e A)) }
[PROOFSTEP]
rintro ⟨Δ₁, α₁⟩ ⟨Δ₂, α₂⟩ h₁
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂ : { α // Epi α }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
⊢ { fst := Δ₁, snd := α₁ } = { fst := Δ₂, snd := α₂ }
[PROOFSTEP]
induction' Δ₁ using Opposite.rec with Δ₁
[GOAL]
case mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂ }
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := Δ₂, snd := α₂ }
[PROOFSTEP]
induction' Δ₂ using Opposite.rec with Δ₂
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁ 
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
have h₂ : Δ₁ = Δ₂ := by
  ext1
  simpa only [Fin.mk_eq_mk] using h₁.1
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ Δ₁ = Δ₂
[PROOFSTEP]
ext1
[GOAL]
case a
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
⊢ len Δ₁ = len Δ₂
[PROOFSTEP]
simpa only [Fin.mk_eq_mk] using h₁.1
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂✝ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂✝, snd := α₂✝ }
Δ₂ : SimplexCategory
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₂ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₂ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₂ }, snd := α₂ }))
h₂ : Δ₁ = Δ₂
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₂ }, snd := α₂ }
[PROOFSTEP]
subst h₂
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ { fst := { unop := Δ₁ }, snd := α₁ } = { fst := { unop := Δ₁ }, snd := α₂ }
[PROOFSTEP]
refine' ext _ _ rfl _
[GOAL]
case mk.mk.mk.mk
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ e { fst := { unop := Δ₁ }, snd := α₁ } ≫
      eqToHom (_ : { fst := { unop := Δ₁ }, snd := α₁ }.fst.unop = { fst := { unop := Δ₁ }, snd := α₂ }.fst.unop) =
    e { fst := { unop := Δ₁ }, snd := α₂ }
[PROOFSTEP]
ext : 2
[GOAL]
case mk.mk.mk.mk.a.h
C : Type u_1
inst✝ : Category.{?u.1648, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁✝ : SimplexCategoryᵒᵖ
α₁✝ : { α // Epi α }
Δ₂ : SimplexCategoryᵒᵖ
α₂✝ : { α // Epi α }
h₁✝² :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
Δ₁ : SimplexCategory
α₁ : { α // Epi α }
h₁✝¹ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₁ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₂, snd := α₂✝ }
α₂ : { α // Epi α }
h₁✝ :
  (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := Δ₁✝, snd := α₁✝ } =
    (fun A =>
        { fst := { val := len A.fst.unop, isLt := (_ : len A.fst.unop < Nat.succ (len Δ.unop)) },
          snd := ↑(Hom.toOrderHom (e A)) })
      { fst := { unop := Δ₁ }, snd := α₂ }
h₁ :
  len Δ₁ = len Δ₁ ∧
    HEq ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₁ }))
      ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
⊢ ↑(Hom.toOrderHom
        (e { fst := { unop := Δ₁ }, snd := α₁ } ≫
          eqToHom
            (_ : { fst := { unop := Δ₁ }, snd := α₁ }.fst.unop = { fst := { unop := Δ₁ }, snd := α₂ }.fst.unop))) =
    ↑(Hom.toOrderHom (e { fst := { unop := Δ₁ }, snd := α₂ }))
[PROOFSTEP]
exact eq_of_heq h₁.2
[GOAL]
C : Type u_1
inst✝ : Category.{?u.3923, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Epi (𝟙 Δ.unop)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ A.fst = Δ
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → A.fst = Δ
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ A.fst = Δ
[PROOFSTEP]
dsimp at h 
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ
[PROOFSTEP]
rw [h]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
[PROOFSTEP]
rfl
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → EqId A
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ EqId A
[PROOFSTEP]
rcases A with ⟨_, ⟨f, hf⟩⟩
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : { fst := fst✝, snd := { val := f, property := hf } }.fst = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
simp only at h 
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : fst✝ = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
subst h
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
[PROOFSTEP]
refine' ext _ _ rfl _
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
[PROOFSTEP]
haveI := hf
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
[PROOFSTEP]
simp only [eqToHom_refl, comp_id]
[GOAL]
case mpr.mk.mk
C : Type u_1
inst✝ : Category.{?u.4321, u_1} C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } = e (id fst✝)
[PROOFSTEP]
exact eq_id_of_epi f
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ len A.fst.unop = len Δ.unop
[PROOFSTEP]
rw [eqId_iff_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ len A.fst.unop = len Δ.unop
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → len A.fst.unop = len Δ.unop
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ len A.fst.unop = len Δ.unop
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → A.fst = Δ
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst = Δ
[PROOFSTEP]
rw [← unop_inj_iff]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst.unop = Δ.unop
[PROOFSTEP]
ext
[GOAL]
case mpr.a
C : Type u_1
inst✝ : Category.{?u.4752, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len A.fst.unop = len Δ.unop
[PROOFSTEP]
exact h
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
rw [eqId_iff_len_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop ↔ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.4880, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len Δ.unop ≤ len A.fst.unop → len A.fst.unop = len Δ.unop
[PROOFSTEP]
exact le_antisymm (len_le_of_epi (inferInstance : Epi A.e))
[GOAL]
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ Mono (e A)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → Mono (e A)
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ Mono (e A)
[PROOFSTEP]
dsimp at h 
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono (e A)
[PROOFSTEP]
subst h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (e (id Δ))
[PROOFSTEP]
dsimp only [id, e]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 Δ.unop)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono (e A) → EqId A
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ EqId A
[PROOFSTEP]
rw [eqId_iff_len_le]
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{?u.5425, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ len Δ.unop ≤ len A.fst.unop
[PROOFSTEP]
exact len_le_of_mono h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
dsimp only [ιSummand, Iso.hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιCoprod s.N A ≫ (iso s Δ).hom = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
erw [colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
n : ℕ
⊢ ιSummand s (IndexSet.id (op [n])) = ι s n
[PROOFSTEP]
erw [ιSummand_eq, X.map_id, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
n : ℕ
⊢ ι s (len (IndexSet.id (op [n])).fst.unop) = ι s n
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ NatTrans.app f Δ = φ s f (len A.fst.unop) ≫ Y.map (IndexSet.e A).op
[PROOFSTEP]
simp only [ιSummand_eq_assoc, φ, assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op ≫ NatTrans.app f Δ =
    ι s (len A.fst.unop) ≫ NatTrans.app f (op [len A.fst.unop]) ≫ Y.map (IndexSet.e A).op
[PROOFSTEP]
erw [NatTrans.naturality]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ f = g
[PROOFSTEP]
rw [← cancel_epi (s.iso Δ).hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
⊢ (iso s Δ).hom ≫ f = (iso s Δ).hom ≫ g
[PROOFSTEP]
ext A
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), ιSummand s A ≫ f = ιSummand s A ≫ g
A : IndexSet Δ
⊢ Sigma.ι (summand s.N Δ) A ≫ (iso s Δ).hom ≫ f = Sigma.ι (summand s.N Δ) A ≫ (iso s Δ).hom ≫ g
[PROOFSTEP]
simpa only [ιSummand_eq, iso_hom, map, colimit.ι_desc_assoc, Cofan.mk_ι_app] using h A
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
⊢ f = g
[PROOFSTEP]
ext Δ
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ NatTrans.app f Δ = NatTrans.app g Δ
[PROOFSTEP]
apply s.hom_ext'
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), ιSummand s A ≫ NatTrans.app f Δ = ιSummand s A ≫ NatTrans.app g Δ
[PROOFSTEP]
intro A
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ NatTrans.app f Δ = ιSummand s A ≫ NatTrans.app g Δ
[PROOFSTEP]
induction' Δ using Opposite.rec with Δ
[GOAL]
case h.h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝ : IndexSet Δ✝
Δ : SimplexCategory
A : IndexSet { unop := Δ }
⊢ ιSummand s A ≫ NatTrans.app f { unop := Δ } = ιSummand s A ≫ NatTrans.app g { unop := Δ }
[PROOFSTEP]
induction' Δ using SimplexCategory.rec with n
[GOAL]
case h.h.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ NatTrans.app f { unop := [n] } = ιSummand s A ≫ NatTrans.app g { unop := [n] }
[PROOFSTEP]
dsimp
[GOAL]
case h.h.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f g : X ⟶ Y
h : ∀ (n : ℕ), φ s f n = φ s g n
Δ✝ : SimplexCategoryᵒᵖ
A✝¹ : IndexSet Δ✝
Δ : SimplexCategory
A✝ : IndexSet { unop := Δ }
n : ℕ
A : IndexSet { unop := [n] }
⊢ ιSummand s A ≫ NatTrans.app f { unop := [n] } = ιSummand s A ≫ NatTrans.app g { unop := [n] }
[PROOFSTEP]
simp only [s.ιSummand_comp_app, h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ ιSummand s A ≫ desc s Δ F = F A
[PROOFSTEP]
dsimp only [ιSummand, desc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ (ιCoprod s.N A ≫ (iso s Δ).hom) ≫ (iso s Δ).inv ≫ Sigma.desc F = F A
[PROOFSTEP]
simp only [assoc, Iso.hom_inv_id_assoc, ιCoprod]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → N s (len A.fst.unop) ⟶ Z
A : IndexSet Δ
⊢ Sigma.ι (summand s.N Δ) A ≫ Sigma.desc F = F A
[PROOFSTEP]
erw [colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ)
[PROOFSTEP]
convert (inferInstance : IsIso ((s.iso Δ).hom ≫ e.hom.app Δ))
[GOAL]
case h.e'_5
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
⊢ map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ = (iso s Δ).hom ≫ NatTrans.app e.hom Δ
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
C : Type u_1
inst✝¹ : Category.{?u.147648, u_1} C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
b✝ : IndexSet Δ
⊢ Sigma.ι (summand (fun n => N s n) Δ) b✝ ≫ map Y (fun n => ι s n ≫ NatTrans.app e.hom (op [n])) Δ =
    Sigma.ι (summand (fun n => N s n) Δ) b✝ ≫ (iso s Δ).hom ≫ NatTrans.app e.hom Δ
[PROOFSTEP]
simp [map]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ ιSummand s A ≫ X.map p = ιSummand s (IndexSet.epiComp A p)
[PROOFSTEP]
dsimp [ιSummand]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (Sigma.ι (fun A => N s (len A.fst.unop)) A ≫ Sigma.desc fun A => ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op) ≫
      X.map p =
    Sigma.ι (fun A => N s (len A.fst.unop)) (IndexSet.epiComp A p) ≫
      Sigma.desc fun A => ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
[PROOFSTEP]
erw [colimit.ι_desc, colimit.ι_desc, Cofan.mk_ι_app, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len { as := A }.as.fst.unop) ≫ X.map (IndexSet.e { as := A }.as).op) ≫ X.map p =
    ι s (len { as := IndexSet.epiComp A p }.as.fst.unop) ≫ X.map (IndexSet.e { as := IndexSet.epiComp A p }.as).op
[PROOFSTEP]
dsimp only [IndexSet.epiComp, IndexSet.e]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len A.fst.unop) ≫ X.map (↑A.snd).op) ≫ X.map p = ι s (len A.fst.unop) ≫ X.map (p.unop ≫ ↑A.snd).op
[PROOFSTEP]
rw [op_comp, X.map_comp, assoc, Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : Hom S₁ S₂
h : ∀ (n : ℕ), f Φ₁ n = f Φ₂ n
⊢ Φ₁ = Φ₂
[PROOFSTEP]
rcases Φ₁ with ⟨F₁, f₁, c₁⟩
[GOAL]
case mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₂ : Hom S₁ S₂
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f Φ₂ n
⊢ mk F₁ f₁ = Φ₂
[PROOFSTEP]
rcases Φ₂ with ⟨F₂, f₂, c₂⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
⊢ mk F₁ f₁ = mk F₂ f₂
[PROOFSTEP]
have h' : f₁ = f₂ := by
  ext
  apply h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
⊢ f₁ = f₂
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
x✝ : ℕ
⊢ f₁ x✝ = f₂ x✝
[PROOFSTEP]
apply h
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₂ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₂) n
h' : f₁ = f₂
⊢ mk F₁ f₁ = mk F₂ f₂
[PROOFSTEP]
subst h'
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ mk F₁ f₁ = mk F₂ f₁
[PROOFSTEP]
simp only [mk.injEq, and_true]
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ F₁ = F₂
[PROOFSTEP]
apply S₁.s.hom_ext
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
⊢ ∀ (n : ℕ), Splitting.φ S₁.s F₁ n = Splitting.φ S₁.s F₂ n
[PROOFSTEP]
intro n
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
n : ℕ
⊢ Splitting.φ S₁.s F₁ n = Splitting.φ S₁.s F₂ n
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → Splitting.N S₁.s n ⟶ Splitting.N S₂.s n
c₁ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n]) = f₁ n ≫ Splitting.ι S₂.s n
h : ∀ (n : ℕ), f (mk F₁ f₁) n = f (mk F₂ f₁) n
n : ℕ
⊢ Splitting.ι S₁.s n ≫ NatTrans.app F₁ (op [n]) = Splitting.ι S₁.s n ≫ NatTrans.app F₂ (op [n])
[PROOFSTEP]
rw [c₁, c₂]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.183784, u_1} C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝ ⟶ Y✝
Φ₂₃ : Y✝ ⟶ Z✝
n : ℕ
⊢ Splitting.ι X✝.s n ≫ NatTrans.app (Φ₁₂.F ≫ Φ₂₃.F) (op [n]) =
    (fun n => Split.Hom.f Φ₁₂ n ≫ Split.Hom.f Φ₂₃ n) n ≫ Splitting.ι Z✝.s n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.183784, u_1} C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝ ⟶ Y✝
Φ₂₃ : Y✝ ⟶ Z✝
n : ℕ
⊢ Splitting.ι X✝.s n ≫ NatTrans.app Φ₁₂.F (op [n]) ≫ NatTrans.app Φ₂₃.F (op [n]) =
    (Split.Hom.f Φ₁₂ n ≫ Split.Hom.f Φ₂₃ n) ≫ Splitting.ι Z✝.s n
[PROOFSTEP]
simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Hom.f Φ₁ n = Hom.f Φ₂ n
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Splitting.ιSummand S₁.s A ≫ NatTrans.app Φ.F Δ = Hom.f Φ (len A.fst.unop) ≫ Splitting.ιSummand S₂.s A
[PROOFSTEP]
erw [S₁.s.ιSummand_eq, S₂.s.ιSummand_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
