awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ (Truncated.Edge.map (𝟙rq x) f).edge =
    Truncated.Edge.edge (x₀ :=
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  Truncated.Edge._proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
        x)
      (x₁ :=
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  Truncated.Edge._proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
        x)
      (𝟙rq
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
            (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := _proof_1 })))
          x))

Tactic:
simp [← NatTrans.naturality_apply, reflQuiver_id]

Premises used: CategoryTheory.NatTrans.naturality_apply, SSet.OneTruncation₂.reflQuiver_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X : Truncated 2
x₁ y₁ x₂ y₂ : OneTruncation₂ X
f : x₁ ⟶ y₁
hx : x₁ = x₂
hy : y₁ = y₂
subst : (Quiver.homOfEq f ⋯ ⋯).edge = f.edge
⊢ (Quiver.homOfEq f hx hy).edge = f.edge

Tactic:
subst hx hy
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X : Truncated 2
x₁ y₁ : OneTruncation₂ X
f : x₁ ⟶ y₁
⊢ (Quiver.homOfEq f ⋯ ⋯).edge = f.edge

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
C : Type u
inst : Category.{v, u} C
X Y : OneTruncation₂ (obj (truncation 2) (nerve.{v, u} C))
f : X ⟶ Y
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C)
      ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) Y : C))
    ((nerveHomEquiv :
          (a : X ⟶ Y) →
            (nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X ⟶
              (nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) Y)
        f :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C)
        ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) Y : C))
    (eqToHom ⋯ ≫ ComposableArrows.hom f.edge ≫ eqToHom ⋯ : ComposableArrows.left X ⟶ ComposableArrows.left Y)

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
C : Type u
inst : Category.{v, u} C
X : OneTruncation₂ (obj (truncation 2) (nerve.{v, u} C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C)
      ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C))
    ((nerveHomEquiv :
          (a : X ⟶ X) →
            (nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X ⟶
              (nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X)
        (𝟙rq X) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C)
        ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C))
    (𝟙 ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C)
        ((nerveEquiv : (a : OneTruncation₂ ((truncation 2).obj (nerve C))) → C) X : C))

Tactic:
nerve.homEquiv_id _

Premises used: CategoryTheory.nerve.homEquiv_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X : Truncated 2
C : Type u
inst : Category.{u, u} C
F G : X ⟶ obj (truncation 2) (nerve C)
h : map F = map G
x₀ x₁ :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Truncated.Edge._proof_1))
f : Truncated.Edge x₀ x₁
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f.edge :
      (fun (X : Type u) ↦ X)
        (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (G.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        f.edge :
      (fun (X : Type u) ↦ X)
        (obj (C := (SimplexCategory.Truncated (HAdd.hAdd (α := ℕ) 1 1))ᵒᵖ) (obj (truncation 2) (nerve C))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
simpa using congr_arg Truncated.Edge.edge (ReflPrefunctor.congr_hom h f)

Premises used: SSet.Truncated.Edge.edge, CategoryTheory.ReflPrefunctor.congr_hom, congr_arg
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Cat
F : X ⟶ Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X_1 : (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u)),
    Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        X_1 =
      Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          (Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                X) ≫
            ReflQuiv.forget.map F))
        X_1
⊢ ∀ (X_1 : (↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X) : Type u)),
    Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫
            Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                Y)))
        X_1 =
      Prefunctor.obj
        (ReflPrefunctor.toPrefunctor
          (Iso.hom
              ((fun (C : Cat.{u, u}) ↦
                  (ofNerve₂ (↑C : Type u) :
                    ReflQuiv.of (OneTruncation₂ (obj (truncation 2) (nerve (↑C : Type u)))) ≅
                      ReflQuiv.of (↑C : Type u)))
                X) ≫
            ReflQuiv.forget.map F))
        X_1

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Cat
F : X ⟶ Y
f :
  (nerveFunctor₂.obj X).obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Truncated.Edge._proof_2))
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((nerveFunctor₂.map F).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌
                  Truncated.Edge._proof_2))) :
          (a : (nerveFunctor₂.obj X).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })) →
            ((truncation 2).obj (nerve (↑Y : Type u))).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 }))
        f) =
    F.toFunctor.map (ComposableArrows.hom f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
C : Type u
inst : Category.{v, u} C
V : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
φ : (fun (X : Type w) ↦ X) (V.obj (op Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (V.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map α.op) :
          (a : (fun (X : Type w) ↦ X) (V.obj (op Y))) → (fun (X : Type w) ↦ X) (V.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map β.op) :
              (a : (fun (X : Type w) ↦ X) (V.obj (op Z))) → (fun (X : Type w) ↦ X) (V.obj (op Y)))
            φ :
          (fun (X : Type w) ↦ X) (V.obj (op Y))) :
      (fun (X : Type w) ↦ X) (V.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (α ≫ β).op) :
          (a : (fun (X : Type w) ↦ X) (V.obj (op Z))) → (fun (X : Type w) ↦ X) (V.obj (op X)))
        φ :
      (fun (X : Type w) ↦ X) (V.obj (op X)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
⊢ (quotientFunctor V).Full

Tactic:
Quotient.full_functor _

Premises used: SSet.Truncated.HomotopyCategory.quotientFunctor, CategoryTheory.Quotient.full_functor, SSet.Truncated.HomotopyCategory
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x : Paths (OneTruncation₂ V)
⊢ ∃ (a :
    V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
    mk a =
      CategoryTheory.Quotient.mk (r := OneTruncation₂.HoRel₂ V)
        (CategoryTheory.Quotient.mk (r := Cat.FreeReflRel (OneTruncation₂ V)) x)

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x : Paths (OneTruncation₂ V)
⊢ ∃ (a :
    V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
    mk a =
      CategoryTheory.Quotient.mk (r := OneTruncation₂.HoRel₂ V)
        (CategoryTheory.Quotient.mk (r := Cat.FreeReflRel (OneTruncation₂ V)) x)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
h :
  x.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
obtain :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    (h :
      (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
        y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))),
    mk x = y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Premises used: SSet.Truncated.HomotopyCategory.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
y : V.HomotopyCategory
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
h :
  (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
obtain :
  ∀
    (y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    (h :
      (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
        (mk y).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))),
    mk x = mk y
⊢ mk x = y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Premises used: SSet.Truncated.HomotopyCategory.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
h :
  (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    (mk y).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
⊢ x = y

Tactic:
h

Premises used: SSet.OneTruncation₂, CategoryTheory.Paths
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
h :
  (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    (mk y).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
obtain : mk x = mk x
⊢ mk x = mk y

Tactic:
obtain rfl : x = y := h

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ mk x = mk x

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
motive : V.HomotopyCategory → Prop
h :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    motive (mk x)
x : V.HomotopyCategory
obtain :
  ∀
    (x' :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    motive (mk x')
⊢ motive x

Tactic:
obtain ⟨x', rfl⟩ := mk_surjective x

Premises used: SSet.Truncated.HomotopyCategory.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
motive : V.HomotopyCategory → Prop
h :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    motive (mk x)
x' :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ motive (mk x')

Tactic:
h x'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
motive : V.HomotopyCategory → Prop
h :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    motive (mk x)
x' :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ motive (mk x')

Tactic:
exact h x'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e.edge =
    y₀
rw₁ :
  Eq (α :=
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
rw₂ rw₃ :
  Eq (α :=
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
⊢ x₀ = y₀

Tactic:
rw [← e.src_eq, ← e'.src_eq, h]

Premises used: SSet.Truncated.Edge.src_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
obtain : ∀ (e' : Edge x₀ y₁) (h : e.edge = e'.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e')
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')

Tactic:
obtain rfl : x₀ = y₀ := by rw [← e.src_eq, ← e'.src_eq, h]

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge x₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e.edge =
    y₁
rw₁ :
  Eq (α :=
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
rw₂ rw₃ :
  Eq (α :=
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
⊢ x₁ = y₁

Tactic:
rw [← e.tgt_eq, ← e'.tgt_eq, h]

Premises used: SSet.Truncated.Edge.tgt_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge x₀ y₁
h : e.edge = e'.edge
obtain : ∀ (e' : Edge x₀ x₁) (h : e.edge = e'.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e')
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')

Tactic:
obtain rfl : x₁ = y₁ := by rw [← e.tgt_eq, ← e'.tgt_eq, h]

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e e' : Edge x₀ x₁
h : e.edge = e'.edge
⊢ e = e'

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e e' : Edge x₀ x₁
h : e.edge = e'.edge
obtain : ∀ (h : e.edge = e.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e)
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')

Tactic:
obtain rfl : e = e' := by aesop

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
h : e.edge = e.edge
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e)

Tactic:
rfl