awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
x y : Ext.{w, v, u} X Y n
⊢ (R.extEquivCohomologyClass : (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
      (x + y) =
    HAdd.hAdd (α := CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)) (β :=
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
          x :
        CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
          y :
        CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
R.extAddEquivCohomologyClass.map_add _ _

Premises used: Function.surjInv, AddEquiv.map_add, Classical.choose, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
x y : Ext.{w, v, u} X Y n
⊢ (R.extEquivCohomologyClass : (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
      (x - y) =
    HSub.hSub (α := CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)) (β :=
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
          x :
        CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
          y :
        CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
R.extAddEquivCohomologyClass.map_sub _ _

Premises used: Function.surjInv, Classical.choose, AddEquiv.map_sub, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
x : Ext.{w, v, u} X Y n
⊢ Eq.{v + 1} (α := CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    ((R.extEquivCohomologyClass :
          (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
        (-x) :
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (-(R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
          x :
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
R.extAddEquivCohomologyClass.map_neg _

Premises used: Function.surjInv, Classical.choose, AddEquiv.map_neg, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
⊢ Eq.{v + 1} (α := CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    ((R.extEquivCohomologyClass :
        (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
      0)
    0

Tactic:
R.extAddEquivCohomologyClass.map_zero

Premises used: AddEquiv.map_zero, Function.surjInv, Classical.choose, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (↑n : ℤ) = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 = -(↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y)
    (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) 0

Tactic:
simpa [cochainComplex_d _ _ _ m n rfl rfl]

Premises used: CategoryTheory.ProjectiveResolution.cochainComplex_d, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq.{v + 1} (α := CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    ((R.extEquivCohomologyClass :
          (a : Ext X Y n) → CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ))
        (R.extMk f m hm hf) :
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯) :
      CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
simp [extMk]

Premises used: CategoryTheory.ProjectiveResolution.extMk
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.complex.d m n ≫ (f + g) = 0

Tactic:
simp [hf, hg]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
simp :
  HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f + (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) (R.extMk g m hm hg) = R.extMk (f + g) m hm ⋯

Tactic:
simp only [extMk, Preadditive.comp_add]

Premises used: CategoryTheory.ProjectiveResolution.extMk, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y)
    (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) 0

Tactic:
simpa [cochainComplex_d _ _ _ m n rfl rfl]

Premises used: CategoryTheory.ProjectiveResolution.cochainComplex_d, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y)
    (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) 0

Tactic:
simpa [cochainComplex_d _ _ _ m n rfl rfl]

Premises used: CategoryTheory.ProjectiveResolution.cochainComplex_d, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
rw :
  HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (HAdd.hAdd (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)))
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f + (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))

Tactic:
rw [Cocycle.toSingleMk_add _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]

Premises used: CochainComplex.HomComplex.Cocycle.toSingleMk_add
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (HAdd.hAdd (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.complex.d m n ≫ (f - g) = 0

Tactic:
simp [hf, hg]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
simp :
  HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f - (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))
⊢ HSub.hSub (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) (R.extMk g m hm hg) = R.extMk (f - g) m hm ⋯

Tactic:
simp only [extMk, Preadditive.comp_sub]

Premises used: CategoryTheory.ProjectiveResolution.extMk, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
rw :
  HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (HSub.hSub (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)))
⊢ HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f - (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))

Tactic:
rw [Cocycle.toSingleMk_sub _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]

Premises used: CochainComplex.HomComplex.Cocycle.toSingleMk_sub
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (HSub.hSub (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)
          (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ R.complex.d m n ≫ (-f) = 0

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
simp :
  Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk (-(R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (-R.extMk f m hm hf) (R.extMk (-f) m hm ⋯)

Tactic:
simp only [extMk, Preadditive.comp_neg]

Premises used: CategoryTheory.ProjectiveResolution.extMk, CategoryTheory.Preadditive.comp_neg
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y)
    (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) 0

Tactic:
simpa [cochainComplex_d _ _ _ m n rfl rfl]

Premises used: CategoryTheory.ProjectiveResolution.cochainComplex_d, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
rw :
  Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk (-(R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)

Tactic:
rw [Cocycle.toSingleMk_neg _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]

Premises used: CochainComplex.HomComplex.Cocycle.toSingleMk_neg
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (-Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : ProjectiveResolution.{v, u} X
n_1 n m : ℕ
hm : n + 1 = m
⊢ Eq (α := R.complex.X m ⟶ Y) (R.complex.d m n ≫ 0) 0

Tactic:
simp