awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ)
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) X))
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
    (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)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯ (inv (Functor.map DerivedCategory.Q R.ι'))) ⋯)
    (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)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯
        (inv (Functor.map DerivedCategory.Q R.ι') ≫ 𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y)))
      ⋯)
have e_g : Eq.{u_1 + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{u_1, v, u} C) (Functor.obj DerivedCategory.Q R.cochainComplex)
    (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)))
  (inv (Functor.map DerivedCategory.Q R.ι'))
  (inv (Functor.map DerivedCategory.Q R.ι') ≫ 𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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) =
    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)
          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)
have have : ∀ (this : HasDerivedCategory C),
  (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (x + 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)
          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: have := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 : ℤ)
this : HasDerivedCategory C
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (x + 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)
          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)
have obtain : ∀ (x : Cocycle (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)
      (CohomologyClass.mk x + 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)
          y :
        Ext.{w, v, u} X Y n)
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 : ℕ
y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
this : HasDerivedCategory C
x : Cocycle (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)
      (CohomologyClass.mk x + 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)
          y :
        Ext.{w, v, u} X Y n)
have obtain : ∀ (y : Cocycle (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)
      (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)
Tactic: obtain ⟨y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 : ℤ)
⊢ (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)
have h : 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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) (R.extMk f m hm hf) (R.extMk g m hm hg) = R.extMk (f + g) m hm ⋯
have 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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv + g ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv)
        sorry (↑m : ℤ) sorry sorry))
Tactic: simp only [extMk, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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
        (Cocycle.fromSingleMk
          (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv + g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
have 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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)
        (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) sorry (↑m : ℤ) sorry sorry)))
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])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 (Cocycle.fromSingleMk ((f - g) ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
have 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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv - g ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv)
        sorry (↑m : ℤ) sorry sorry))
Tactic: simp only [Preadditive.sub_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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
        (Cocycle.fromSingleMk
          (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv - g ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯))
have 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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
      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 sorry).inv) sorry (↑m : ℤ) sorry sorry)
        (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) sorry (↑m : ℤ) sorry sorry)))
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])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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.{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)
          (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 ((-f) ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
have simp : 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)
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
    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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
    Ext.{w, v, u} X Y n)
Tactic: simp only [Preadditive.neg_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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.{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)
          (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 (-f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯)) :
      Ext.{w, v, u} X Y n)
have rw : 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)
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
    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 sorry).inv) sorry (↑m : ℤ) sorry sorry)) :
    Ext.{w, v, u} X Y n)
Tactic: rw [Cocycle.fromSingleMk_neg _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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
p : ℕ
hp : p + 1 = n
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) 0 ↔ ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
have simp : Membership.mem (γ := AddSubgroup (Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)))
    (coboundaries (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
    (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) sorry (↑m : ℤ) sorry sorry) ↔
  ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
Tactic: simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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
p : ℕ
hp : p + 1 = n
⊢ Membership.mem (γ := AddSubgroup (Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)))
      (coboundaries (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ))
      (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯) ↔
    ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
have rw : (∃ (g : X ⟶ R.cochainComplex.X (↑p : ℤ)),
    g ≫ (R.cochainComplexXIso (↑p : ℤ) p sorry).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv =
      f ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) ↔
  ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
Tactic: rw [Cocycle.fromSingleMk_mem_coboundaries_iff _ _ _ _ _ p (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (goal)
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 : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ (f : X ⟶ R.cocomplex.X n) (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = α
have obtain : ∀ (x : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)),
  ∃ (f : X ⟶ R.cocomplex.X n) (hf : f ≫ R.cocomplex.d n m = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
        x)
Tactic: obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α
Cleared hypotheses: α