awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑m : ℤ)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ))
    ((f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0

Tactic:
simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]

Premises used: rfl, CategoryTheory.InjectiveResolution.cochainComplex_d
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ HAdd.hAdd (α := ℤ) 0 (↑n : ℤ) + 0 = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 0 + 0 = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (b := (↑n : ℤ))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g))
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X)) ⋯)
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
            (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        ⋯)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X'))
      (ShiftedHom.comp (b := (↑n : ℤ))
        (ShiftedHom.map (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) g)) DerivedCategory.Q)
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                  (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
              (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯
            (inv (Functor.map DerivedCategory.Q R.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
          ⋯)
        ⋯)
      ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n_1 n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
⊢ (f ≫ φ.hom.f n) ≫ R'.cocomplex.d n m = 0

Tactic:
simp [reassoc_of% hf]
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
have :
  ∀ (this : HasDerivedCategory C),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯)
      (R'.extMk (f ≫ φ.hom.f n) m hm ⋯)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯) (R'.extMk (f ≫ φ.hom.f n) m hm ⋯)

Tactic:
have := HasDerivedCategory.standard C
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (Ext.hom (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯)) (Ext.hom (R'.extMk (f ≫ φ.hom.f n) m hm ⋯))
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯) (R'.extMk (f ≫ φ.hom.f n) m hm ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ Eq (α := ℤ) (↑n : ℤ) (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)

Tactic:
simp [φ.hom'_f n n rfl]

Premises used: CategoryTheory.InjectiveResolution.Hom.hom'_f, Nat.cast, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)

Tactic:
have : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso n n (by lia)).inv =
      (f ≫ (R.cochainComplexXIso n n (by lia)).inv) ≫ φ.hom'.f n := by
    simp [φ.hom'_f n n rfl]
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                  (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
              (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯
            (inv (Functor.map DerivedCategory.Q R.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
          ⋯)
        ⋯)
      (ShiftedHom.mk₀ (↑0 : ℤ) Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g)) ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle ((singleFunctor C 0).obj X) R'.cochainComplex (↑n : ℤ)) →
                (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R'.cochainComplex)
            (Cocycle.fromSingleMk ((f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (inv (Functor.map DerivedCategory.Q R'.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (Ext.hom (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯)) (Ext.hom (R'.extMk (f ≫ φ.hom.f n) m hm ⋯))

Tactic:
simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, this]

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.InjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑m : ℤ)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ))
    ((f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0

Tactic:
simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]

Premises used: rfl, CategoryTheory.InjectiveResolution.cochainComplex_d
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑0 : ℤ) (↑n : ℤ) + 0 = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑0 : ℤ) 0 + (↑n : ℤ) = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ HAdd.hAdd (α := ℤ) 0 0 + (↑n : ℤ) = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
h :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y) ≫
      Functor.map (DerivedCategory.singleFunctor C 0) g)
    (Functor.map DerivedCategory.Q φ.hom' ≫
      inv (Functor.map DerivedCategory.Q R'.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp (b := (↑n : ℤ))
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
            (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (Functor.map DerivedCategory.Q R.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y) ≫
            Functor.map (DerivedCategory.singleFunctor C 0) g))
        ⋯)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
                (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
            (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (Functor.map DerivedCategory.Q φ.hom' ≫
            inv (Functor.map DerivedCategory.Q R'.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)

Tactic:
congr 3
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
h :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
    ((Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι')) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y) ≫
      Functor.map (DerivedCategory.singleFunctor C 0) g)
    (Functor.map DerivedCategory.Q φ.hom' ≫
      inv (Functor.map DerivedCategory.Q R'.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')

Tactic:
rw [Category.assoc, ← NatTrans.naturality, ← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
h :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (singleFunctor C 0 ⋙ DerivedCategory.Q) Y'))
    (inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g)
    (Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι'))
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
    ((Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι')) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : InjectiveResolution.{v, u} Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (singleFunctor C 0 ⋙ DerivedCategory.Q) Y'))
    (inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g)
    (Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι'))

Tactic:
simpa only [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
    Functor.map_comp] using DerivedCategory.Q.congr_map φ.ι'_comp_hom'.symm

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, DerivedCategory.Q, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, Eq.symm, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ CochainComplex.IsStrictlyGE (HomologicalComplex.extend R.cocomplex ComplexShape.embeddingUpNat) 0

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n₁ n₂ : ℤ
k₁ k₂ : ℕ
h₁ : (↑k₁ : ℤ) = n₁
h₂ : (↑k₂ : ℤ) = n₂
⊢ R.cochainComplex.d n₁ n₂ =
    (R.cochainComplexXIso n₁ k₁ h₁).hom ≫ R.cocomplex.d k₁ k₂ ≫ (R.cochainComplexXIso n₂ k₂ h₂).inv

Tactic:
HomologicalComplex.extend_d_eq _ _ h₁ h₂

Premises used: HomologicalComplex.extend_d_eq
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
pos : ∀ (hn : 0 ≤ n), Injective.{v, u} (R.cochainComplex.X n)
neg : ∀ (hn : ¬0 ≤ n), Injective.{v, u} (R.cochainComplex.X n)
⊢ Injective.{v, u} (R.cochainComplex.X n)

Tactic:
by_cases hn : 0 ≤ n
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
hn : 0 ≤ n
pos : ∀ (k : ℕ) (hn : LE.le (α := ℤ) 0 (↑k : ℤ)), Injective.{v, u} (R.cochainComplex.X (↑k : ℤ))
⊢ Injective.{v, u} (R.cochainComplex.X n)

Tactic:
obtain ⟨k, rfl⟩ := Int.eq_ofNat_of_zero_le hn

Premises used: Int.eq_ofNat_of_zero_le, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
k : ℕ
hn : LE.le (α := ℤ) 0 (↑k : ℤ)
⊢ Injective.{v, u} (R.cochainComplex.X (↑k : ℤ))

Tactic:
Injective.of_iso (R.cochainComplexXIso _ _ rfl).symm inferInstance

Premises used: CategoryTheory.Injective.of_iso, inferInstance, CategoryTheory.Iso.symm, rfl, CategoryTheory.InjectiveResolution.cochainComplexXIso
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
k : ℕ
hn : LE.le (α := ℤ) 0 (↑k : ℤ)
⊢ Injective.{v, u} (R.cochainComplex.X (↑k : ℤ))

Tactic:
exact Injective.of_iso (R.cochainComplexXIso _ _ rfl).symm inferInstance

Premises used: CategoryTheory.Injective.of_iso, inferInstance, CategoryTheory.Iso.symm, rfl, CategoryTheory.InjectiveResolution.cochainComplexXIso
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
hn : ¬0 ≤ n
⊢ n < 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
hn : ¬0 ≤ n
⊢ Injective.{v, u} (R.cochainComplex.X n)

Tactic:
exact IsZero.injective (CochainComplex.isZero_of_isStrictlyGE _ 0 _ (by lia))

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.injective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ ComplexShape.embeddingUpNat.f 0 = 0

Tactic:
simp