awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ (F.leftDerived n).map f ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
    Iso.hom (P.isoLeftDerivedObj F n) ≫
      Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ
have dsimp : Eq (α :=
  Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
    HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (Functor.map F.leftDerivedToHomotopyCategory f) ≫
    Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex))
  ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
    HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)
Tactic: dsimp [isoLeftDerivedObj, Functor.leftDerived]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map
            (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)) φ) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)
have erw : Eq (α :=
  Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
    HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
    NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
      Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
    NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
      HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)
Tactic: erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ ≫
      Iso.inv (Q.isoLeftDerivedObj F n)
have rw : (Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f) ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
  CategoryStruct.comp (Y := (F.leftDerived n).obj Y)
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ ≫
      Iso.inv (Q.isoLeftDerivedObj F n))
    (Iso.hom (Q.isoLeftDerivedObj F n))
Tactic: rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, assoc, assoc,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
rw :
  (Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f) ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
    CategoryStruct.comp (Y := (F.leftDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          φ ≫
        Iso.inv (Q.isoLeftDerivedObj F n))
      (Iso.hom (Q.isoLeftDerivedObj F n))
⊢ Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ ≫
      Iso.inv (Q.isoLeftDerivedObj F n)
have rw₁ : Iso.inv (P.isoLeftDerivedObj F n) ≫ (F.leftDerived n).map f ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
  CategoryStruct.comp (Y := (F.leftDerived n).obj Y)
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ ≫
      Iso.inv (Q.isoLeftDerivedObj F n))
    (Iso.hom (Q.isoLeftDerivedObj F n))
Tactic: rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, assoc, assoc,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
⊢ IsZero.{v_1, u_1} ((F.leftDerived (n + 1)).obj X)
have refine : IsZero.{v_1, u_1}
  (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
    (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1))
    (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
      (ProjectiveResolution.complex (ProjectiveResolution.self X))))
Tactic: refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
⊢ IsZero.{v_1, u_1}
    (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (ProjectiveResolution.self X))))
have erw : HomologicalComplex.ExactAt
  (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
    (ProjectiveResolution.complex (ProjectiveResolution.self X)))
  (n + 1)
Tactic: erw [← HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
⊢ (F.leftDerived n).map f =
    Iso.hom (P.isoLeftDerivedObj F n) ≫
      map
          (comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          g ≫
        Iso.inv (Q.isoLeftDerivedObj F n)
have rw : Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
  (P.π.f 0 ≫ f)
Tactic: rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,
    assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
have rw : Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) ((g ≫ Q.π).f 0)
  (P.π.f 0 ≫ f)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
rw :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) ((g ≫ Q.π).f 0)
    (P.π.f 0 ≫ f)
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
have rw₁ : Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
  ((P.π ≫ map (ChainComplex.single₀ C) f).f 0) (P.π.f 0 ≫ f)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
rw :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) ((g ≫ Q.π).f 0)
    (P.π.f 0 ≫ f)
rw₁ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    ((P.π ≫ map (ChainComplex.single₀ C) f).f 0) (P.π.f 0 ≫ f)
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
have rw₂ : Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
  (P.π.f 0 ≫ HomologicalComplex.Hom.f (map (ChainComplex.single₀ C) f) 0) (P.π.f 0 ≫ f)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
rw :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) ((g ≫ Q.π).f 0)
    (P.π.f 0 ≫ f)
rw₁ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    ((P.π ≫ map (ChainComplex.single₀ C) f).f 0) (P.π.f 0 ≫ f)
rw₂ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    (P.π.f 0 ≫ HomologicalComplex.Hom.f (map (ChainComplex.single₀ C) f) 0) (P.π.f 0 ≫ f)
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
have rw₃ : Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (P.π.f 0 ≫ f) (P.π.f 0 ≫ f)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X) (Functor.obj G.leftDerivedToHomotopyCategory X))
    (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X)
    (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G))
have rw : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
    (Functor.obj F.leftDerivedToHomotopyCategory X)
    (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
      P.complex))
  (CategoryStruct.comp (Y := Functor.obj G.leftDerivedToHomotopyCategory X)
      (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X) (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj G)) :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex))
  (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex))
Tactic: rw [← cancel_mono (P.isoLeftDerivedToHomotopyCategoryObj G).hom, assoc, assoc,
      Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ Functor.whiskerRight (leftDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (F.leftDerived n)
have simp : 𝟙
    (Functor.comp (D := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ)) F.leftDerivedToHomotopyCategory
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)) =
  𝟙 (F.leftDerived n)
Tactic: simp only [leftDerivedToHomotopyCategory_id, Functor.whiskerRight_id']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
n : ℕ
⊢ Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X) (NatTrans.app (NatTrans.leftDerived α n) X)
    (Iso.hom (P.isoLeftDerivedObj F n) ≫
      Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        Iso.inv (P.isoLeftDerivedObj G n))
have dsimp : Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
    (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X))
  ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
    HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n ≫
      NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
Tactic: dsimp [NatTrans.leftDerived, isoLeftDerivedObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
n : ℕ
⊢ Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
            (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
have rw : Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
    Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
  (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
    NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
            (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
Tactic: rw [ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, Functor.map_comp, assoc]