awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
erw :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ })
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫
          𝟙 { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }

Tactic:
erw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
rw :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X)
rw₁ rw₂ :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X) (NatTrans.app Γ₂N₁.natTrans X)
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      { X := X, p := 𝟙 X, idem := ⋯ })
    (NatTrans.app Γ₂N₁.natTrans X)
    (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ })

Tactic:
rw [comp_id, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P)))
          n ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
          n)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
            (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
            (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))))
        n)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₂ P))) n)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y := Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.N₂_obj_p_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
have eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫
      ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
    simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
eq₁ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    Splitting.summand
        (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
        (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor
          (Splitting.summand
            (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
            (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
        (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))) n))
    (HomologicalComplex.Hom.f PInfty n ≫ P.p.app (op ⦋n⦌))

Tactic:
have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) := by
    dsimp
    rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
    dsimp
    rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
    dsimp [toKaroubi]
    rw [Splitting.ι_desc_assoc]
    simp [Splitting.IndexSet.e]
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
eq₁ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))
eq₂ :
  Eq (α :=
    Splitting.summand
        (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
        (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor
          (Splitting.summand
            (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
            (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
        (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))) n))
    (HomologicalComplex.Hom.f PInfty n ≫ P.p.app (op ⦋n⦌))
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₂ P))) n)

Tactic:
simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_f, N₂_obj_p_f, assoc,
    eq₁, eq₂, PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, HomologicalComplex.comp_f, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.Idempotents.app_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
w :
  ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
    Eq (α :=
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Functor.obj (N₂ ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) P)
        (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C)) ⋙ N₂) P))
      (NatTrans.app
        (CategoryStruct.comp (Y := Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ (Γ₂ ⋙ N₂))
          (𝟙 N₂ ◫ Iso.inv N₂Γ₂) (Iso.inv (Functor.associator N₂ Γ₂ N₂) ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂))
        P)
      (NatTrans.app (𝟙 N₂) P)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (N₂ ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C)) ⋙ N₂))
    (CategoryStruct.comp (Y := Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ (Γ₂ ⋙ N₂))
      (𝟙 N₂ ◫ Iso.inv N₂Γ₂) (Iso.inv (Functor.associator N₂ Γ₂ N₂) ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂))
    (𝟙 N₂)

Tactic:
ext P : 2

Premises used: AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y := Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))

Tactic:
have h := identity_N₂_objectwise P
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (Functor.obj N₂ P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))

Tactic:
rw [hom_comp_eq_id] at h

Premises used: CategoryTheory.hom_comp_eq_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (Functor.obj N₂ P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
rw :
  IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (Functor.obj N₂ P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))

Tactic:
have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
this :
  IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
    (NatTrans.app Γ₂N₂.natTrans P)

Tactic:
isIso_of_reflects_iso _ N₂

Premises used: CategoryTheory.isIso_of_reflects_iso, AlgebraicTopology.DoldKan.N₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
this :
  IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
    (NatTrans.app Γ₂N₂.natTrans P)

Tactic:
exact isIso_of_reflects_iso _ N₂

Premises used: CategoryTheory.isIso_of_reflects_iso, AlgebraicTopology.DoldKan.N₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
⊢ ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
    IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
      (NatTrans.app Γ₂N₂.natTrans P)

Tactic:
have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) := by
    intro P
    have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
    exact isIso_of_reflects_iso _ N₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
this :
  ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
    IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
      (NatTrans.app Γ₂N₂.natTrans P)
⊢ IsIso (C := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ Karoubi (SimplicialObject.{v_1, u_1} C)) (X :=
    Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) Γ₂N₂.natTrans

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
rw :
  IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
    (NatTrans.app Γ₂N₁.natTrans X)

Tactic:
rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]

Premises used: AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
⊢ ∀ (X : SimplicialObject.{v_1, u_1} C),
    IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
      (NatTrans.app Γ₂N₁.natTrans X)

Tactic:
have : ∀ X : SimplicialObject C, IsIso (Γ₂N₁.natTrans.app X) := by
    intro X
    rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
this :
  ∀ (X : SimplicialObject.{v_1, u_1} C),
    IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
      (NatTrans.app Γ₂N₁.natTrans X)
⊢ IsIso (C := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C)) (X :=
    Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) Γ₂N₁.natTrans

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
this : ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
⊢ ∀ (Δ : SimplexCategoryᵒᵖ), IsIso (f.app Δ)

Tactic:
haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
this_1 : ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
this : ∀ (Δ : SimplexCategoryᵒᵖ), IsIso (f.app Δ)
⊢ IsIso f

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
suffices : ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
⊢ IsIso f

Tactic:
suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌)) by
      haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
      apply NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
⊢ ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)

Tactic:
have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))