awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
⊢ spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
    spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y
have h₁ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      i =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      i =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow i
have h₁ : Path.arrow
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩) =
  (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
h₁ :
  Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))
⊢ Path.arrow
      (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
        (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
      i =
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow i
have h₃ : Path.arrow
    (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4
      (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩) =
  (spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y).arrow
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
f : Edge x y
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) = eqToHom ⋯ ≫ F.map (homMk f) ≫ eqToHom ⋯
have dsimp : (descOfTruncation (homToNerveMk F)).map (homMk f) =
  𝟙
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
        ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0)) ≫
    F.map (homMk f) ≫ 𝟙 (F.obj (mk y))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
f : Edge x y
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) =
    𝟙
        ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) (F.obj (mk x)) : ComposableArrows C 0)) ≫
      F.map (homMk f) ≫ 𝟙 (F.obj (mk y))
have simp : (nerve.homEquiv :
      (a :
          SSet.Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x)))
            ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y)))) →
        (nerveEquiv : (a : ComposableArrows C 0) → C)
            ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk x))) ⟶
          (nerveEquiv : (a : ComposableArrows C 0) → C)
            ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) (F.obj (mk y))))
    (f.map (homToNerveMk F)) =
  F.map (homMk f)
Tactic: simp only [Category.comp_id, Category.id_comp, descOfTruncation_map_homMk,
        homToNerveMk_app_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
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)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        x₀)
      0)
    (ComposableArrows.left (n := 1)
      ((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))
have refine_1 : Eq.{u + 1} (α := C)
  (Functor.obj (C := Fin 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 1 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)
  (ComposableArrows.left (n := 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ sorry))) :
        (a : X.obj (op { obj := ⦋1⦌, property := sorry })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := sorry }))
      f.edge))
Tactic: simp only [← f.src_eq, NatTrans.naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
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)
            (φ.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : X.obj (op { obj := ⦋0⦌, property := _proof_1 })) →
            ((truncation 2).obj (nerve C)).obj (op { obj := ⦋0⦌, property := _proof_1 }))
        x₁)
      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)
have refine_2 : 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⦌ sorry))) :
        (a : X.obj (op { obj := ⦋1⦌, property := sorry })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := sorry }))
      f.edge)
    1)
Tactic: simp only [← f.tgt_eq, NatTrans.naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
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₁
⊢ 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⦌ ⋯)))
have 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⦌ sorry))) :
      (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := sorry })) →
        ((truncation 2).obj (nerve D)).obj (op { obj := ⦋1⦌, property := sorry }))
    (ComposableArrows.mk₁ (F.map (homMk f)))
Tactic: simp only [homToNerveMk_app_edge, Functor.comp_obj, Functor.comp_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X' X : Truncated 2
Y : Cat
x : X' ⟶ X
x_1 : X ⟶ nerveFunctor₂.obj Y
⊢ 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)
have 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))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
X Y : Cat
x : X ⟶ Y
⊢ (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom = x
have h : (functorOfNerveMap (nerveFunctor₂.map x)).toCatHom.toFunctor = x.toFunctor
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (hypothesis)
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)))
have 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))
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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (hypothesis)
Goal:
C D : Type u
inst : Category.{u, u} C
inst_1 : Category.{u, u} D
⊢ IsIso (X := hoFunctor.obj (nerve C ⨯ nerve D)) (Y := hoFunctor.obj (nerve C) ⨯ hoFunctor.obj (nerve D))
    (prodComparison hoFunctor (nerve C) (nerve D))
have 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)))
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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
⊢ IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
    (Y :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
      hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
    (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
      (prodComparisonNatTrans hoFunctor D))
have rw : ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
  IsIso (X :=
    Functor.obj
      ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
        Functor.obj prod.functor D ⋙ hoFunctor)
      X_1)
    (Y :=
    Functor.obj
      ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
        hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
      X_1)
    (NatTrans.app
      (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
        (prodComparisonNatTrans hoFunctor D))
      X_1)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (hypothesis)
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
⊢ IsIso (X := hoFunctor.obj (D ⨯ X)) (Y := hoFunctor.obj D ⨯ hoFunctor.obj X) (prodComparison hoFunctor D X)
have this : IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
  (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
  (Y :=
  (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
    hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
  (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
    (prodComparisonNatTrans hoFunctor D))
Tactic: have : IsIso (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda X ⋙ uliftYoneda)
      (prodComparisonNatTrans hoFunctor.{u} D)) := by
    rw [NatTrans.isIso_iff_isIso_app]
    exact fun x ↦ H (x.left).len
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X Y : SSet
m : ℕ
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
have h : Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
  (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
    (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
      (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
Tactic: convert_to IsIso (hoFunctor.map (prod.braiding _ _).hom ≫
    prodComparison hoFunctor Δ[m] X ≫ (prod.braiding _ _).hom)