awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : X ⟶ Functor.obj (truncation 2) (nerve C)
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
⊢ Eq.{u + 1} (α := C)
    (Functor.obj (C := Fin 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (φ.app
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2)
                      ⦋HAdd.hAdd (α := ℕ) 0 1⦌ Edge._proof_3))) :
              (a : X.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                Edge._proof_3))))
      0)
    (Functor.obj (C := Fin 2)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge)
      1)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
simp :
  ComposableArrows.mk₁ (G.map (F.map (homMk f))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (CategoryTheory.Functor.map (truncation 2) (nerveMap G))
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })) →
          ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
      (ComposableArrows.mk₁ (F.map (homMk f)))
⊢ Eq (α :=
    Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((homToNerveMk (F ⋙ G)).app
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        f.edge :
      Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (CategoryTheory.Functor.map (truncation 2) (nerveMap G))
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
          (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })) →
            ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((homToNerveMk F).app
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
              (a : X.obj (op { obj := ⦋1⦌, property := ⋯ })) →
                ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ }))
            f.edge :
          Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
      Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve D))
        (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯)))

Tactic:
simp only [homToNerveMk_app_edge, Functor.comp_obj, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (G.map (F.map (homMk f)))).hom =
    eqToHom ⋯ ≫
      ComposableArrows.hom
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (CategoryTheory.Functor.map (truncation 2) (nerveMap G))
                  (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
              (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })) →
                ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
            (ComposableArrows.mk₁ (F.map (homMk f)))) ≫
        eqToHom ⋯

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X : Truncated 2
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
f : Edge x₀ x₁
⊢ ComposableArrows.mk₁ (G.map (F.map (homMk f))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (CategoryTheory.Functor.map (truncation 2) (nerveMap G))
            (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := ⋯ })) →
          ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := ⋯ }))
      (ComposableArrows.mk₁ (F.map (homMk f)))

Tactic:
exact ComposableArrows.ext₁ rfl rfl (by aesop)

Premises used: CategoryTheory.ComposableArrows.ext₁, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X' X : Truncated 2
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ nerveFunctor₂.obj Y
h :
  Eq (α := (↑(hoFunctor₂.obj X') : Type u) ⥤ (↑Y : Type u))
    (Cat.Hom.toFunctor
      ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X') Y) HomotopyCategory.functorEquiv) :
          (a : X' ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X' ⟶ Y)
        (x ≫ x_1)))
    (Cat.Hom.toFunctor
      (hoFunctor₂.map x ≫
        (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X) Y) HomotopyCategory.functorEquiv) :
            (a : X ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X ⟶ Y)
          x_1))
⊢ Eq (α := hoFunctor₂.obj X' ⟶ Y)
    ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X') Y) HomotopyCategory.functorEquiv) :
          (a : X' ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X' ⟶ Y)
        (x ≫ x_1) :
      hoFunctor₂.obj X' ⟶ Y)
    (hoFunctor₂.map x ≫
        (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X) Y) HomotopyCategory.functorEquiv) :
            (a : X ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X ⟶ Y)
          x_1 :
      hoFunctor₂.obj X' ⟶ Y)

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X' X : Truncated 2
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ nerveFunctor₂.obj Y
⊢ Eq (α := (↑(hoFunctor₂.obj X') : Type u) ⥤ (↑Y : Type u))
    (Cat.Hom.toFunctor
      ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X') Y) HomotopyCategory.functorEquiv) :
          (a : X' ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X' ⟶ Y)
        (x ≫ x_1)))
    (Cat.Hom.toFunctor
      (hoFunctor₂.map x ≫
        (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X) Y) HomotopyCategory.functorEquiv) :
            (a : X ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X ⟶ Y)
          x_1))

Tactic:
HomotopyCategory.descOfTruncation_comp _ _

Premises used: SSet.Truncated.HomotopyCategory.descOfTruncation_comp, SSet.Truncated.HomotopyCategory.lift, CategoryTheory.Functor.comp, SSet.Truncated.HomotopyCategory.descOfTruncation, SSet.Truncated.HomotopyCategory, CategoryTheory.Quotient.lift
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X' X : Truncated 2
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ nerveFunctor₂.obj Y
⊢ Eq (α := (↑(hoFunctor₂.obj X') : Type u) ⥤ (↑Y : Type u))
    (Cat.Hom.toFunctor
      ((Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X') Y) HomotopyCategory.functorEquiv) :
          (a : X' ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X' ⟶ Y)
        (x ≫ x_1)))
    (Cat.Hom.toFunctor
      (hoFunctor₂.map x ≫
        (Equiv.symm (Equiv.trans (Cat.Hom.equivFunctor (hoFunctor₂.obj X) Y) HomotopyCategory.functorEquiv) :
            (a : X ⟶ nerveFunctor₂.obj Y) → hoFunctor₂.obj X ⟶ Y)
          x_1))

Tactic:
exact HomotopyCategory.descOfTruncation_comp _ _

Premises used: SSet.Truncated.HomotopyCategory.descOfTruncation_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ ⦋0⦌.len ≤ 2

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x y : (↑(Cat.of C) : Type u)
f : x ⟶ y
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((nerveFunctor₂.obj (Cat.of D)).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((nerveFunctor₂.map (functorOfNerveMap φ).toCatHom).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        (ComposableArrows.mk₁ f) :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        (ComposableArrows.mk₁ f) :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
(nerveMap_app_mk₁ _ _).trans ((nerve.mk₁_homEquiv_apply _).trans
      (ComposableArrows.mk₁_hom _))

Premises used: CategoryTheory.ComposableArrows.mk₁_hom, CategoryTheory.nerve.mk₁_homEquiv_apply, CategoryTheory.nerveMap_app_mk₁, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x y : (↑(Cat.of C) : Type u)
f : x ⟶ y
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((nerveFunctor₂.obj (Cat.of D)).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((nerveFunctor₂.map (functorOfNerveMap φ).toCatHom).app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        (ComposableArrows.mk₁ f) :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (φ.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
                  ⋯))) :
          (a : (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋1⦌, property := ⋯ })))
        (ComposableArrows.mk₁ f) :
      (fun (X : Type u) ↦ X)
        ((nerveFunctor₂.obj (Cat.of D)).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ HAdd.hAdd (α := ℕ) 1 1) ⦋1⦌
              ⋯))))

Tactic:
exact (nerveMap_app_mk₁ _ _).trans ((nerve.mk₁_homEquiv_apply _).trans
      (ComposableArrows.mk₁_hom _))

Premises used: CategoryTheory.nerveMap_app_mk₁, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
x : C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) x = F.obj x
⊢ Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) x = F.obj x

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
x y : C
f : x ⟶ y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := D) (Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) x)
      (Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) y))
    (Functor.map (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) f) (eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := D) (Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) x)
      (Functor.obj (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) y))
    (Functor.map (functorOfNerveMap (Functor.map (SSet.truncation 2) (nerveMap F))) f) (eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯)

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
X Y : Cat
x : X ⟶ Y
h : (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom.toFunctor = x.toFunctor
⊢ (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom = x

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
X Y : Cat
x : X ⟶ Y
⊢ (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom.toFunctor = x.toFunctor

Tactic:
functorOfNerveMap_nerveFunctor₂_map _

Premises used: CategoryTheory.Cat, CategoryTheory.nerve.functorOfNerveMap, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
X Y : Cat
x : X ⟶ Y
⊢ (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom.toFunctor = x.toFunctor

Tactic:
exact functorOfNerveMap_nerveFunctor₂_map _

Premises used: CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
⊢ nerveFunctor₂.Faithful

Tactic:
(fullyFaithfulNerveFunctor₂).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.nerve.fullyFaithfulNerveFunctor₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
⊢ nerveFunctor₂.Full

Tactic:
(fullyFaithfulNerveFunctor₂).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.nerve.fullyFaithfulNerveFunctor₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
⊢ nerveFunctor.Faithful

Tactic:
Functor.Faithful.of_iso Nerve.cosk₂Iso.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Nerve.cosk₂Iso, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
⊢ nerveFunctor.Full

Tactic:
Functor.Full.of_iso Nerve.cosk₂Iso.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.Full.of_iso, CategoryTheory.Nerve.cosk₂Iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
⊢ IsIso nerveAdjunction.counit

Tactic:
Adjunction.counit_isIso_of_R_fully_faithful _

Premises used: CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
iso : nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor ≅ nerveFunctor :=
  (nerveFunctor.associator hoFunctor nerveFunctor).symm ≪≫
    Functor.isoWhiskerRight nerveFunctorCompHoFunctorIso nerveFunctor ≪≫ nerveFunctor.leftUnitor
⊢ IsIso (X := (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of C ⨯ Cat.of D)) (Y :=
    (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of C) ⨯ (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of D))
    (prodComparison (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor) (Cat.of C) (Cat.of D))

Tactic:
IsIso.of_isIso_fac_right (prodComparison_natural_of_natTrans iso.hom).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.Limits.prodComparison_natural_of_natTrans, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
iso : nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor ≅ nerveFunctor :=
  (nerveFunctor.associator hoFunctor nerveFunctor).symm ≪≫
    Functor.isoWhiskerRight nerveFunctorCompHoFunctorIso nerveFunctor ≪≫ nerveFunctor.leftUnitor
⊢ IsIso (X := (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of C ⨯ Cat.of D)) (Y :=
    (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of C) ⨯ (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor).obj (Cat.of D))
    (prodComparison (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor) (Cat.of C) (Cat.of D))

Tactic:
exact IsIso.of_isIso_fac_right (prodComparison_natural_of_natTrans iso.hom).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.Limits.prodComparison_natural_of_natTrans, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
⊢ hoFunctor.IsLeftAdjoint

Tactic:
nerveAdjunction.isLeftAdjoint

Premises used: CategoryTheory.nerveAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
⊢ IsIso (X := (hoFunctor ⋙ nerveFunctor).obj (nerve C ⨯ nerve D)) (Y :=
    (hoFunctor ⋙ nerveFunctor).obj (nerve C) ⨯ (hoFunctor ⋙ nerveFunctor).obj (nerve D))
    (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D))

Tactic:
have : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D)) :=
      IsIso.of_isIso_fac_left
        (prodComparison_comp nerveFunctor (hoFunctor ⋙ nerveFunctor)
          (A := Cat.of C) (B := Cat.of D)).symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
this :
  IsIso (X := (hoFunctor ⋙ nerveFunctor).obj (nerve C ⨯ nerve D)) (Y :=
    (hoFunctor ⋙ nerveFunctor).obj (nerve C) ⨯ (hoFunctor ⋙ nerveFunctor).obj (nerve D))
    (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D))
⊢ IsIso (X := nerveFunctor.obj (hoFunctor.obj (nerve C ⨯ nerve D))) (Y :=
    nerveFunctor.obj (hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D)))
    (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm

Premises used: CategoryTheory.Limits.prodComparison_comp, CategoryTheory.nerveFunctor, CategoryTheory.IsIso.of_isIso_fac_right, Eq.symm, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
this :
  IsIso (X := (hoFunctor ⋙ nerveFunctor).obj (nerve C ⨯ nerve D)) (Y :=
    (hoFunctor ⋙ nerveFunctor).obj (nerve C) ⨯ (hoFunctor ⋙ nerveFunctor).obj (nerve D))
    (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D))
⊢ IsIso (X := nerveFunctor.obj (hoFunctor.obj (nerve C ⨯ nerve D))) (Y :=
    nerveFunctor.obj (hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D)))
    (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
exact IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm

Premises used: CategoryTheory.Limits.prodComparison_comp, CategoryTheory.nerveFunctor, CategoryTheory.IsIso.of_isIso_fac_right, Eq.symm, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
⊢ IsIso (X := nerveFunctor.obj (hoFunctor.obj (nerve C ⨯ nerve D))) (Y :=
    nerveFunctor.obj (hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D)))
    (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
have : IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D))) := by
    have : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D)) :=
      IsIso.of_isIso_fac_left
        (prodComparison_comp nerveFunctor (hoFunctor ⋙ nerveFunctor)
          (A := Cat.of C) (B := Cat.of D)).symm
    exact IsIso.of_isIso_fac_right (prodComparison_comp hoFunctor nerveFunctor).symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
this :
  IsIso (X := nerveFunctor.obj (hoFunctor.obj (nerve C ⨯ nerve D))) (Y :=
    nerveFunctor.obj (hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D)))
    (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))
⊢ IsIso (X := hoFunctor.obj (nerve C ⨯ nerve D)) (Y := hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D))
    (prodComparison hoFunctor (nerve C) (nerve D))

Tactic:
isIso_of_fully_faithful nerveFunctor _

Premises used: CategoryTheory.isIso_of_fully_faithful, CategoryTheory.nerveFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
this :
  IsIso (X := nerveFunctor.obj (hoFunctor.obj (nerve C ⨯ nerve D))) (Y :=
    nerveFunctor.obj (hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D)))
    (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))
⊢ IsIso (X := hoFunctor.obj (nerve C ⨯ nerve D)) (Y := hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D))
    (prodComparison hoFunctor (nerve C) (nerve D))

Tactic:
exact isIso_of_fully_faithful nerveFunctor _

Premises used: CategoryTheory.isIso_of_fully_faithful, CategoryTheory.nerveFunctor