awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
e_1 :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
    (obj x₀ ⟶ obj x₂)
e_4 :
  Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
      (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₁) =
    obj x₁
e_5 :
  Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
      (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂) =
    obj x₂
⊢ CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₁₂)) =
    map e₁₂

Tactic:
apply Cat.FreeRefl.lift'_map

Premises used: CategoryTheory.Cat.FreeRefl.lift'_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
e_1 :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
    (obj x₀ ⟶ obj x₂)
⊢ CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₂)) =
    map e₀₂

Tactic:
apply Cat.FreeRefl.lift'_map

Premises used: CategoryTheory.Cat.FreeRefl.lift'_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (lift obj
          (fun
              {x y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))} ↦
            map)
          map_id ⋯).obj
      (mk x) =
    obj x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x y
⊢ (lift obj
          (fun
              {x y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))} ↦
            map)
          map_id ⋯).map
      (homMk e) =
    map e

Tactic:
Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
φ :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x x_1 : V.HomotopyCategory
f : x ⟶ x_1
⊢ Eq.{u + 1} (α := MorphismProperty V.HomotopyCategory)
    (MorphismProperty.naturalityProperty.{u, v_1, u, u_1} (D := D) (F₁ := F) (F₂ := G) fun (x : V.HomotopyCategory) ↦
      φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1))
    ⊤

Tactic:
have : MorphismProperty.naturalityProperty (fun (x : V.HomotopyCategory) ↦ φ _) = ⊤ :=
      morphismProperty_eq_top (fun e ↦ hφ e)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
φ :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x x_1 : V.HomotopyCategory
f : x ⟶ x_1
this :
  Eq.{u + 1} (α := MorphismProperty V.HomotopyCategory)
    (MorphismProperty.naturalityProperty.{u, v_1, u, u_1} (D := D) (F₁ := F) (F₂ := G) fun (x : V.HomotopyCategory) ↦
      φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1))
    ⊤
⊢ ⊤ f

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
φ :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x x_1 : V.HomotopyCategory
f : x ⟶ x_1
this :
  Eq.{u + 1} (α := MorphismProperty V.HomotopyCategory)
    (MorphismProperty.naturalityProperty.{u, v_1, u, u_1} (D := D) (F₁ := F) (F₂ := G) fun (x : V.HomotopyCategory) ↦
      φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1))
    ⊤
⊢ F.map f ≫ φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x_1.1) =
    φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1) ≫ G.map f

Tactic:
exact this.symm.le f (by simp)

Premises used: Eq.le, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
φ :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
v :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (mkNatTrans φ hφ).app (mk v) = φ v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
iso :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ≅ G.obj (mk x)
hiso :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ (iso y).hom = (iso x).hom ≫ G.map (homMk e)
v :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (mkNatIso iso hiso).hom.app (mk v) = (iso v).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
iso :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ≅ G.obj (mk x)
hiso :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ (iso y).hom = (iso x).hom ≫ G.map (homMk e)
v :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (mkNatIso iso hiso).inv.app (mk v) = (iso v).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
h₁ :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    F.obj (mk x) = G.obj (mk x)
h₂ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) = eqToHom ⋯ ≫ G.map (homMk e) ≫ eqToHom ⋯
x x_1 :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x x_1
⊢ F.map (homMk e) ≫
      Iso.hom
        ((fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (eqToIso ⋯ : F.obj (mk x) ≅ G.obj (mk x)))
          x_1) =
    Iso.hom
        ((fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (eqToIso ⋯ : F.obj (mk x) ≅ G.obj (mk x)))
          x) ≫
      G.map (homMk e)

Tactic:
simp [h₂ e]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
x y : X.HomotopyCategory
obtain :
  ∀
    (x :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    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 W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
y : X.HomotopyCategory
x :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
obtain :
  ∀
    (y :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    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 W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
obtain : mk x = mk x
⊢ mk x = mk y

Tactic:
obtain rfl := Subsingleton.elim x y

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
x :
  X.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 W X : Truncated 2
inst :
  Unique
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
inst_1 :
  Subsingleton.{u + 1}
    (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ι0₂._proof_5)))
x y : X.HomotopyCategory
⊢ Subsingleton.{u + 1} (x ⟶ y)

Tactic:
letI : Unique (OneTruncation₂ X) := inferInstanceAs (Unique (X _⦋0⦌₂))
  letI (x y : (OneTruncation₂ X)) : Subsingleton (x ⟶ y) :=
    inferInstanceAs (Subsingleton <| X.Edge _ _)
  CategoryTheory.Quotient.instSubsingletonHom _ _ _

Premises used: CategoryTheory.Quotient.instSubsingletonHom, SSet.OneTruncation₂.HoRel₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X : Truncated 2
inst :
  Unique
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
inst_1 :
  Subsingleton.{u + 1}
    (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ι0₂._proof_5)))
⊢ ∀ {X_1 Y : X.HomotopyCategory} (f : X_1 ⟶ Y), X_1 = Y

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
f : V ⟶ W
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ Eq (α :=
    (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).obj
        (obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).obj
        (obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂))
    ((((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V))
        (CategoryStruct.comp (Y := x₁) (Quiver.Hom.toPath e₀₁) (Quiver.Hom.toPath e₁₂))))
    ((((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₂)))

Tactic:
CategoryTheory.Quotient.sound _ ⟨h.map f⟩

Premises used: SSet.Truncated.Edge.CompStruct.map, SSet.OneTruncation₂.HoRel₂.of_compStruct, CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
f : V ⟶ W
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ Eq (α :=
    (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).obj
        (obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).obj
        (obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂))
    ((((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V))
        (CategoryStruct.comp (Y := x₁) (Quiver.Hom.toPath e₀₁) (Quiver.Hom.toPath e₁₂))))
    ((((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₂)))

Tactic:
exact CategoryTheory.Quotient.sound _ ⟨h.map f⟩

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
f : V ⟶ W
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ (mapHomotopyCategory f).obj (HomotopyCategory.mk x) =
    HomotopyCategory.mk
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) →
            (fun (X : Type u) ↦ X) (W.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })))
        x)

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
f : V ⟶ W
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x y
⊢ (mapHomotopyCategory f).map (homMk e) = homMk (e.map f)

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, Quiver.Path.comp, rfl, SSet.Truncated.Edge.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W x : Truncated 2
h : (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor = Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))
⊢ (mapHomotopyCategory (𝟙 x)).toCatHom = 𝟙 (Cat.of x.HomotopyCategory)

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W x : Truncated 2
⊢ ∀
    (x_1 :
      x.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor.obj (HomotopyCategory.mk x_1) =
      (Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))).obj (HomotopyCategory.mk x_1)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W x : Truncated 2
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀
    ⦃x_1 y :
      x.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x_1 y),
    (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫ (Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))).map (HomotopyCategory.homMk e) ≫ eqToHom ⋯
⊢ ∀
    ⦃x_1 y :
      x.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x_1 y),
    (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫ (Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))).map (HomotopyCategory.homMk e) ≫ eqToHom ⋯

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W x : Truncated 2
⊢ (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor = Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))

Tactic:
exact HomotopyCategory.functor_ext (by simp) (by cat_disch)

Premises used: SSet.Truncated.HomotopyCategory.functor_ext