awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
let : ∀ (s₁ : f.CompStruct g' h'), HomotopicL h h'
⊢ HomotopicL h h'

Tactic:
let ⟨s₁⟩ := Quasicategory₂.fill32 hf (idComp g') s'
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
s₁ : f.CompStruct g' h'
let : ∀ (s₂ : f.CompStruct g h'), HomotopicL h h'
⊢ HomotopicL h h'

Tactic:
let ⟨s₂⟩ := Quasicategory₂.fill31 (compId f) hg s₁
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
s₁ : f.CompStruct g' h'
s₂ : f.CompStruct g h'
⊢ HomotopicL h h'

Tactic:
Quasicategory₂.fill31 s (compId g) s₂

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
s₁ : f.CompStruct g' h'
s₂ : f.CompStruct g h'
⊢ HomotopicL h h'

Tactic:
exact Quasicategory₂.fill31 s (compId g) s₂

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α :=
    A.obj
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
          Quasicategory₂._proof_1)))
    mk

Tactic:
fun ⟨x⟩ ↦ ⟨x, rfl⟩

Premises used: _private.0.SSet.Truncated.HomotopyCategory₂.mk_surjective.match_1, Exists, Exists.intro, SSet.Truncated.HomotopyCategory₂.mk, Eq, Function.Surjective, rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := Edge x y) (β := { pt := x : A.HomotopyCategory₂ } ⟶ { pt := y }) homMk

Tactic:
Quotient.mk_surjective

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.HomotopyCategory₂.Hom, Quotient, Quotient.mk_surjective
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x : A.HomotopyCategory₂
⊢ Eq (α := { pt := x.pt : A.HomotopyCategory₂ } ⟶ { pt := x.pt }) (homMk (Edge.id x.pt)) (𝟙 x)

Tactic:
rfl

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, Quotient.mk', rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicL f g
⊢ Eq (α := { pt := x : A.HomotopyCategory₂ } ⟶ { pt := y }) (homMk f) (homMk g)

Tactic:
Quotient.sound h

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.HomotopyCategory₂.Hom, Quotient, Quotient.sound
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicR f g
⊢ Eq (α := { pt := x : A.HomotopyCategory₂ } ⟶ { pt := y }) (homMk f) (homMk g)

Tactic:
Quotient.sound h.homotopicL

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.HomotopyCategory₂.Hom, Quotient, Quotient.sound, SSet.Truncated.HomotopicR.homotopicL
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
g : Edge y z
h : Edge x z
s : f.CompStruct g h
⊢ Eq (α := { pt := x : A.HomotopyCategory₂ } ⟶ { pt := z }) (homMk f ≫ homMk g) (homMk h)

Tactic:
(comp_unique (compStruct _ _) s .refl .refl).congr_homotopyCategory₂HomMk

Premises used: SSet.Truncated.HomotopicL.refl, SSet.Truncated.Edge.CompStruct.comp_unique, SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.Edge.compStruct, SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
g : Edge y z
h : Edge x z
fac : ⟦f.comp g⟧ = ⟦h⟧
⊢ f.comp g ≈ h

Tactic:
rw [Quotient.eq_iff_equiv] at fac

Premises used: Quotient.eq_iff_equiv
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
g : Edge y z
h : Edge x z
fac : f.comp g ≈ h
⊢ f.CompStruct g h

Tactic:
exact (Quasicategory₂.fill32 (compStruct f g) (compId g) fac.some).some

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.compStruct, SSet.Truncated.Edge.CompStruct.compId, Nonempty.some
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
g : Edge y z
h : Edge x z
⊢ Nonempty.{u_1 + 1} (f.CompStruct g h) ↔
    Eq (α := { pt := x : A.HomotopyCategory₂ } ⟶ { pt := z }) (homMk f ≫ homMk g) (homMk h)

Tactic:
⟨fun ⟨h⟩ ↦ h.homotopyCategory₂_fac, fun h ↦ ⟨.ofHomotopyCategory₂Fac h⟩⟩

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, _private.0.SSet.Truncated.Edge.CompStruct.comp_unique.match_1, Nonempty.intro, SSet.Truncated.Edge.CompStruct.ofHomotopyCategory₂Fac, Iff.intro, CategoryTheory.CategoryStruct.comp, Eq, SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
X Y : A.HomotopyCategory₂
f_1 : X ⟶ Y
f : Edge X.pt Y.pt
⊢ Eq (α := X ⟶ Y) (𝟙 X ≫ Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)
    (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)

Tactic:
((compStruct _ f).comp_unique (idComp _) .refl .refl).congr_homotopyCategory₂HomMk

Premises used: SSet.Truncated.HomotopicL.refl, SSet.Truncated.Edge.CompStruct.comp_unique, SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.Edge.compStruct, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
X Y : A.HomotopyCategory₂
f_1 : X ⟶ Y
f : Edge X.pt Y.pt
⊢ Eq (α := X ⟶ Y) (𝟙 X ≫ Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)
    (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)

Tactic:
exact ((compStruct _ f).comp_unique (idComp _) .refl .refl).congr_homotopyCategory₂HomMk

Premises used: SSet.Truncated.HomotopicL.refl, SSet.Truncated.Edge.CompStruct.comp_unique, SSet.Truncated.Edge.compStruct, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
X Y : A.HomotopyCategory₂
f_1 : X ⟶ Y
f : Edge X.pt Y.pt
⊢ Eq (α := X ⟶ Y) (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f ≫ 𝟙 Y)
    (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)

Tactic:
((compStruct _ _).comp_unique (compId _) .refl .refl).congr_homotopyCategory₂HomMk

Premises used: SSet.Truncated.HomotopicL.refl, SSet.Truncated.Edge.CompStruct.comp_unique, SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.Edge.compStruct, SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
X Y : A.HomotopyCategory₂
f_1 : X ⟶ Y
f : Edge X.pt Y.pt
⊢ Eq (α := X ⟶ Y) (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f ≫ 𝟙 Y)
    (Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) f)

Tactic:
exact ((compStruct _ _).comp_unique (compId _) .refl .refl).congr_homotopyCategory₂HomMk

Premises used: SSet.Truncated.HomotopicL.refl, SSet.Truncated.Edge.CompStruct.comp_unique, SSet.Truncated.Edge.compStruct, SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
W X Y Z : A.HomotopyCategory₂
f_1 : W ⟶ X
f : Edge W.pt X.pt
g_1 : X ⟶ Y
g : Edge X.pt Y.pt
h_1 : Y ⟶ Z
h : Edge Y.pt Z.pt
⊢ Eq.{u_1 + 1} (α := W ⟶ Z)
    ((Quot.mk (⇑(instSetoidEdge W.pt X.pt) : Edge W.pt X.pt → Edge W.pt X.pt → Prop) f ≫
        Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) g) ≫
      Quot.mk (⇑(instSetoidEdge Y.pt Z.pt) : Edge Y.pt Z.pt → Edge Y.pt Z.pt → Prop) h)
    (Quot.mk (⇑(instSetoidEdge W.pt X.pt) : Edge W.pt X.pt → Edge W.pt X.pt → Prop) f ≫
      Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) g ≫
        Quot.mk (⇑(instSetoidEdge Y.pt Z.pt) : Edge Y.pt Z.pt → Edge Y.pt Z.pt → Prop) h)

Tactic:
(Quasicategory₂.fill31 (compStruct f g) (compStruct g h)
      (compStruct _ _)).some.homotopyCategory₂_fac

Premises used: SSet.Truncated.HomotopyCategory₂.homMk, SSet.Truncated.Edge.compStruct, Nonempty.some, SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
W X Y Z : A.HomotopyCategory₂
f_1 : W ⟶ X
f : Edge W.pt X.pt
g_1 : X ⟶ Y
g : Edge X.pt Y.pt
h_1 : Y ⟶ Z
h : Edge Y.pt Z.pt
⊢ Eq.{u_1 + 1} (α := W ⟶ Z)
    ((Quot.mk (⇑(instSetoidEdge W.pt X.pt) : Edge W.pt X.pt → Edge W.pt X.pt → Prop) f ≫
        Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) g) ≫
      Quot.mk (⇑(instSetoidEdge Y.pt Z.pt) : Edge Y.pt Z.pt → Edge Y.pt Z.pt → Prop) h)
    (Quot.mk (⇑(instSetoidEdge W.pt X.pt) : Edge W.pt X.pt → Edge W.pt X.pt → Prop) f ≫
      Quot.mk (⇑(instSetoidEdge X.pt Y.pt) : Edge X.pt Y.pt → Edge X.pt Y.pt → Prop) g ≫
        Quot.mk (⇑(instSetoidEdge Y.pt Z.pt) : Edge Y.pt Z.pt → Edge Y.pt Z.pt → Prop) h)

Tactic:
exact (Quasicategory₂.fill31 (compStruct f g) (compStruct g h)
      (compStruct _ _)).some.homotopyCategory₂_fac

Premises used: SSet.Truncated.Edge.compStruct, Nonempty.some, SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ X.δ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
simp [δ₀Iter]

Premises used: CategoryTheory.SimplicialObject.δ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (X.δ₀Iter 1 ⋯) (X.δ 0)

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, SimplexCategory.mkHom, SimplexCategory.δ, OrderEmbedding.toOrderHom, CategoryTheory.SimplicialObject.δ, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + i = m
⊢ X.δ₀Iter (i + 1) ⋯ = X.δ 0 ≫ X.δ₀Iter i h

Tactic:
simp [δ₀Iter, SimplexCategory.δ₀Iter_succ _ h, δ_def]

Premises used: CategoryTheory.SimplicialObject.δ_def, CategoryTheory.SimplicialObject.δ₀Iter, SimplexCategory.δ₀Iter_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
dsimp :
  X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))
⊢ X.δ₀Iter (i + 1) h = X.δ₀Iter i ⋯ ≫ X.δ 0

Tactic:
dsimp [δ, δ₀Iter]

Premises used: CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map ((SimplexCategory.δ₀Iter i ⋯).op ≫ Quiver.Hom.op (SimplexCategory.δ 0))
rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op
rw₂ rw₃ :
  X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op =
    X.map (SimplexCategory.δ 0 ≫ SimplexCategory.δ₀Iter i ⋯).op
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op =
    X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (Quiver.Hom.op (SimplexCategory.δ 0))

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, SimplexCategory.δ₀Iter_succ'
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
dsimp :
  X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
⊢ X.δ j ≫ X.δ₀Iter i hi = X.δ₀Iter (i + 1) ⋯

Tactic:
dsimp [δ, δ₀Iter]

Premises used: CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.δ j).op ≫ (SimplexCategory.δ₀Iter i hi).op) = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
rw₁ : X.map (SimplexCategory.δ₀Iter i hi ≫ SimplexCategory.δ j).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
rw₂ rw₃ : X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, SimplexCategory.δ₀Iter_δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + j
dsimp :
  X.map (SimplexCategory.δ i').op ≫ X.map (SimplexCategory.δ₀Iter j ⋯).op =
    X.map (SimplexCategory.δ₀Iter j ⋯).op ≫ X.map (SimplexCategory.δ i).op
⊢ X.δ i' ≫ X.δ₀Iter j ⋯ = X.δ₀Iter j ⋯ ≫ X.δ i

Tactic:
dsimp [δ, δ₀Iter]

Premises used: CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : (↑i' : ℕ) = (↑i : ℕ) + j
⊢ X.map (SimplexCategory.δ i').op ≫ X.map (SimplexCategory.δ₀Iter j ⋯).op =
    X.map (SimplexCategory.δ₀Iter j ⋯).op ≫ X.map (SimplexCategory.δ i).op

Tactic:
simp only [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ' _ _ _ _ hi'']

Premises used: CategoryTheory.op_comp, SimplexCategory.δ₀Iter_δ', CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
dsimp :
  X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
⊢ X.σ j ≫ X.δ₀Iter (i + 1) hi = X.δ₀Iter i ⋯

Tactic:
dsimp [σ, δ₀Iter]

Premises used: CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
rw : X.map ((SimplexCategory.σ j).op ≫ (SimplexCategory.δ₀Iter (i + 1) hi).op) = X.map (SimplexCategory.δ₀Iter i ⋯).op
rw₁ : X.map (SimplexCategory.δ₀Iter (i + 1) hi ≫ SimplexCategory.σ j).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
rw₂ rw₃ : X.map (SimplexCategory.δ₀Iter i ⋯).op = X.map (SimplexCategory.δ₀Iter i ⋯).op
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ₀Iter_σ, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + i = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + i
⊢ X.σ j ≫ X.δ₀Iter i ⋯ = X.δ₀Iter i hi' ≫ X.σ j'

Tactic:
simp [σ, δ₀Iter, ← Functor.map_comp, ← op_comp,
    SimplexCategory.δ₀Iter_σ' i j j']

Premises used: CategoryTheory.op_comp, SimplexCategory.δ₀Iter_σ', CategoryTheory.SimplicialObject.δ₀Iter, CategoryTheory.Functor.map_comp, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ X.σ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
simp [σ₀Iter]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ₀Iter 1 ⋯) (X.σ 0)

Tactic:
simp [σ₀Iter, σ_def]

Premises used: CategoryTheory.SimplicialObject.σ_def, CategoryTheory.SimplicialObject.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
dsimp :
  X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op
⊢ X.σ₀Iter (i + 1) h = X.σ 0 ≫ X.σ₀Iter i ⋯

Tactic:
dsimp [σ, σ₀Iter]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + (i + 1) = m
rw :
  X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0) ≫ (SimplexCategory.σ₀Iter i ⋯).op)
rw₁ : X.map (SimplexCategory.σ₀Iter (i + 1) h).op = X.map (SimplexCategory.σ₀Iter i ⋯ ≫ SimplexCategory.σ 0).op
rw₂ rw₃ :
  X.map (SimplexCategory.σ₀Iter i ⋯ ≫ SimplexCategory.σ 0).op =
    X.map (SimplexCategory.σ₀Iter i ⋯ ≫ SimplexCategory.σ 0).op
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op =
    X.map (Quiver.Hom.op (SimplexCategory.σ 0)) ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ₀Iter_succ ..]

Premises used: CategoryTheory.op_comp, SimplexCategory.σ₀Iter_succ, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
h : n + i = m
⊢ X.σ₀Iter (i + 1) ⋯ = X.σ₀Iter i h ≫ X.σ 0

Tactic:
simp [σ₀Iter, SimplexCategory.σ₀Iter_succ' _ h, σ_def]

Premises used: CategoryTheory.SimplicialObject.σ_def, SimplexCategory.σ₀Iter_succ', CategoryTheory.SimplicialObject.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : (↑i : ℕ) ≤ j + 1
⊢ X.σ₀Iter (j + 1) h ≫ X.δ i = X.σ₀Iter j ⋯

Tactic:
simp only [σ₀Iter, δ, ← Functor.map_comp, ← op_comp, SimplexCategory.δ_σ₀Iter i j h]

Premises used: CategoryTheory.op_comp, SimplexCategory.δ_σ₀Iter, CategoryTheory.Functor.map_comp, CategoryTheory.SimplicialObject.σ₀Iter, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < (↑i : ℕ)
hi'' : (↑i : ℕ) = (↑i' : ℕ) + j
⊢ X.σ₀Iter j ⋯ ≫ X.δ i = X.δ i' ≫ X.σ₀Iter j ⋯

Tactic:
simp only [σ₀Iter, δ, ← Functor.map_comp, ← op_comp,
    SimplexCategory.δ_σ₀Iter' i j i']

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.SimplicialObject.σ₀Iter, SimplexCategory.δ_σ₀Iter', CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
dsimp :
  X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ₀Iter (i + 1) ⋯

Tactic:
dsimp [σ, σ₀Iter]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter, CategoryTheory.SimplicialObject.σ