awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₃ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₄ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₅ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (g ≫
          CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (J.cocomplex.d n (n + 1))
            (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₆ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1)) (g ≫ 0) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₇ : HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1)) 0 -
    I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I : InjectiveResolution.{v, u} X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)
have g_comm : I.ι ≫ desc (𝟙 X) I I = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι
Tactic: apply descHomotopy (𝟙 X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I : InjectiveResolution.{v, u} X
g_comm : I.ι ≫ desc (𝟙 X) I I = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)
have h_comm : I.ι ≫ 𝟙 I.cocomplex = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι
Tactic: apply descHomotopy (𝟙 X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
K : InjectiveResolution.{v, u} Z
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)
have g_comm : I.ι ≫ desc (f ≫ g) K I = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι
Tactic: apply descHomotopy (f ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
K : InjectiveResolution.{v, u} Z
g_comm : I.ι ≫ desc (f ≫ g) K I = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)
have h_comm : I.ι ≫ desc f J I ≫ desc g K J = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι
Tactic: apply descHomotopy (f ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (𝟙 (InjectiveResolution.cocomplex (injectiveResolution X))))
have h : Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X))
  (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X))
  (𝟙 (InjectiveResolution.cocomplex (injectiveResolution X)))
Tactic: apply HomotopyCategory.eq_of_homotopy
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution Z))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z) (injectiveResolution X)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (CategoryStruct.comp (Y := InjectiveResolution.cocomplex (injectiveResolution Y))
        (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))
        (InjectiveResolution.desc g (injectiveResolution Z) (injectiveResolution Y))))
have h : Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X)) (D :=
  InjectiveResolution.cocomplex (injectiveResolution Z))
  (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z) (injectiveResolution X))
  (CategoryStruct.comp (Y := InjectiveResolution.cocomplex (injectiveResolution Y))
    (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))
    (InjectiveResolution.desc g (injectiveResolution Z) (injectiveResolution Y)))
Tactic: apply HomotopyCategory.eq_of_homotopy
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
⊢ Eq (α :=
    Functor.obj (injectiveResolutions C) X ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
    (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso)
    (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)
have h : Homotopy (C := cocomplex (injectiveResolution X))
  (CategoryStruct.comp (Y :=
    Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
    (desc f (injectiveResolution Y) (injectiveResolution X))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J)))
  (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ)
Tactic: apply HomotopyCategory.eq_of_homotopy
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
⊢ Homotopy (C := cocomplex (injectiveResolution X))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
      (desc f (injectiveResolution Y) (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J)))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ)
have h : CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
      (desc f (injectiveResolution Y) (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J))) =
  Functor.map (CochainComplex.single₀ C) f ≫ J.ι
Tactic: apply descHomotopy f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
h :
  CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
      (CategoryStruct.comp (Y :=
        Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
        (desc f (injectiveResolution Y) (injectiveResolution X))
        (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J))) =
    Functor.map (CochainComplex.single₀ C) f ≫ J.ι
⊢ Homotopy (C := cocomplex (injectiveResolution X))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
      (desc f (injectiveResolution Y) (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J)))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ)
have h₁ : CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ) =
  Functor.map (CochainComplex.single₀ C) f ≫ J.ι
Tactic: apply descHomotopy f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw : CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₁ : CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
    (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₂ : CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
    (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₃ : Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₃ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₄ : Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y) (Iso.inv J.iso) (Iso.hom J.iso)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₃ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₄ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
      CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y) (Iso.inv J.iso) (Iso.hom J.iso)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₅ : Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
    𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]