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 : ℕ
this : HasDerivedCategory C
x y : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk x + CohomologyClass.mk y)))
    (HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk x) :
          Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk y) :
          Ext.{w, v, u} X Y n)).hom

Tactic:
simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

Premises used: CategoryTheory.ShiftedHom.map, CochainComplex.HomComplex.CohomologyClass.mk_add, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_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 : ℕ
⊢ ∀ (x y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)),
    Equiv.toFun (Equiv.symm R.extEquivCohomologyClass) (x + y) =
      HAdd.hAdd (α := Ext.{w, v, u} X Y n) (Equiv.toFun (Equiv.symm R.extEquivCohomologyClass) x)
        (Equiv.toFun (Equiv.symm R.extEquivCohomologyClass) 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 : ℕ
x y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (x - y) =
    HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)

Tactic:
R.extAddEquivCohomologyClass.symm.map_sub _ _

Premises used: CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, AddEquiv.map_sub, AddEquiv.symm
-- 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 : ℕ
x : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
        (-x) :
      Ext.{w, v, u} X Y n)
    (-(Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          x :
      Ext.{w, v, u} X Y n)

Tactic:
R.extAddEquivCohomologyClass.symm.map_neg _

Premises used: CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, AddEquiv.map_neg, AddEquiv.symm
-- 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 : ℕ
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      0)
    0

Tactic:
R.extAddEquivCohomologyClass.symm.map_zero

Premises used: AddEquiv.map_zero, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, AddEquiv.symm
-- 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 : ℕ
x y : Ext.{w, v, u} X Y n
⊢ (R.extEquivCohomologyClass : (a : Ext X Y n) → CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ))
      (x + y) =
    HAdd.hAdd (α := CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)) (β :=
      CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ))
          x :
        CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
      ((R.extEquivCohomologyClass :
            (a : Ext X Y n) → CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ))
          y :
        CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))

Tactic:
R.extAddEquivCohomologyClass.map_add _ _

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

Tactic:
R.extAddEquivCohomologyClass.map_sub _ _

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

Tactic:
R.extAddEquivCohomologyClass.map_neg _

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

Tactic:
R.extAddEquivCohomologyClass.map_zero

Premises used: AddEquiv.map_zero, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass, Function.surjInv, Classical.choose
-- 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
⊢ 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_1 n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ 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
⊢ Eq.{v + 1} (α := CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
    ((R.extEquivCohomologyClass :
          (a : Ext X Y n) → CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ))
        (R.extMk f m hm hf) :
      CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
    (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯) :
      CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))

Tactic:
simp [extMk]

Premises used: CategoryTheory.InjectiveResolution.extMk
-- 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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f + g) ≫ R.cocomplex.d n m = 0

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

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.InjectiveResolution.extMk
-- 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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ 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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ))
    ((g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0

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

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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
rw :
  HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (HAdd.hAdd (α := Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
          (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)
          (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)))
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.fromSingleMk
          (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv + g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))

Tactic:
rw [Cocycle.fromSingleMk_add _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]

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

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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f - g) ≫ R.cocomplex.d n m = 0

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

Tactic:
simp only [Preadditive.sub_comp]

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

Tactic:
rw [Cocycle.fromSingleMk_sub _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]

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

Tactic:
simp