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

Tactic:
simp [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
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 ⋯).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)
⊢ 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)

Tactic:
simp only [Preadditive.neg_comp]

Premises used: CategoryTheory.Preadditive.neg_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 : 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
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 ⋯).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)
⊢ 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)

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

Premises used: CochainComplex.HomComplex.Cocycle.fromSingleMk_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 : ℕ
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)

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

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 m : ℕ
hm : n + 1 = m
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk 0 m hm ⋯) 0

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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
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
inst_3 : HasDerivedCategory.{u_1, v, u} C
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom.{u_1, w, v, u} (R.extMk f m hm hf))
    (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))
        ⋯)
      ⋯)

Tactic:
extEquivCohomologyClass_symm_mk_hom _ _

Premises used: CategoryTheory.InjectiveResolution.extMk, 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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
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 ⋯).inv) ⋯ (↑m : ℤ) ⋯ ⋯) ↔
    ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
⊢ 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

Tactic:
simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, Equiv.apply_eq_iff_eq, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ HAdd.hAdd (α := ℤ) (↑p : ℤ) 1 = (↑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
p : ℕ
hp : p + 1 = n
rw :
  (∃ (g : X ⟶ R.cochainComplex.X (↑p : ℤ)),
      g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ↔
    ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
⊢ 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

Tactic:
rw [Cocycle.fromSingleMk_mem_coboundaries_iff _ _ _ _ _ p (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]

Premises used: Nat.cast, CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff, 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
p : ℕ
hp : p + 1 = n
h :
  ∃ (g : X ⟶ R.cochainComplex.X (↑p : ℤ)),
    g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
      f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv
g : X ⟶ R.cochainComplex.X (↑p : ℤ)
hg :
  g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv
⊢ (g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom) ≫ R.cocomplex.d p n = f

Tactic:
simp only [← cancel_mono (R.cochainComplexXIso n n rfl).inv, Category.assoc, hg]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, Nat.cast, CategoryTheory.Iso.inv, rfl, CategoryTheory.InjectiveResolution.cochainComplexXIso
-- 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
p : ℕ
hp : p + 1 = n
h : ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f
g : X ⟶ R.cocomplex.X p
hg : g ≫ R.cocomplex.d p n = f
⊢ (g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).inv) ≫
      (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv

Tactic:
simp [← 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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ (g : X ⟶ R.cochainComplex.X (↑p : ℤ)),
      g ≫ (R.cochainComplexXIso (↑p : ℤ) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ↔
    ∃ (g : X ⟶ R.cocomplex.X p), g ≫ R.cocomplex.d p n = f

Tactic:
exact ⟨fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).hom,
      by simp only [← cancel_mono (R.cochainComplexXIso n n rfl).inv, Category.assoc, hg]⟩,
    fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).inv, by simp [← 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 : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
hm : n + 1 = m
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)
⊢ ∃ (f : X ⟶ R.cocomplex.X n) (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = α

Tactic:
obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α

Premises used: CategoryTheory.InjectiveResolution.extEquivCohomologyClass, Equiv.surjective, Equiv.symm, 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 m : ℕ
hm : n + 1 = m
x : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
obtain :
  ∀ (x : Cocycle (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)
          (CohomologyClass.mk x))
⊢ ∃ (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⟩ := x.mk_surjective

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

Tactic:
obtain ⟨f, hf, rfl⟩ := Cocycle.fromSingleMk_surjective x n (by simp) m (by lia)

Premises used: CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective, 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 m : ℕ
hm : n + 1 = m
f : X ⟶ R.cochainComplex.X (↑n : ℤ)
hf : Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ)) (f ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0
⊢ (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).hom) ≫ R.cocomplex.d n m = 0

Tactic:
simpa [R.cochainComplex_d _ _ _ _ rfl rfl,
      ← cancel_mono (R.cochainComplexXIso m m rfl).inv] using hf

Premises used: CategoryTheory.cancel_mono, Nat.cast, CategoryTheory.Iso.inv, rfl, CategoryTheory.InjectiveResolution.cochainComplexXIso, 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 m : ℕ
hm : n + 1 = m
f : X ⟶ R.cochainComplex.X (↑n : ℤ)
hf : Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ)) (f ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).hom) m hm ⋯)
    ((Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk (Cocycle.fromSingleMk f ⋯ (↑m : ℤ) ⋯ hf)))

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 m : ℕ
hm : n + 1 = m
f : X ⟶ R.cochainComplex.X (↑n : ℤ)
hf : Eq (α := X ⟶ R.cochainComplex.X (↑m : ℤ)) (f ≫ R.cochainComplex.d (↑n : ℤ) (↑m : ℤ)) 0
⊢ ∃ (f_1 : X ⟶ R.cocomplex.X n) (hf_1 : f_1 ≫ R.cocomplex.d n m = 0),
    Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f_1 m hm hf_1)
      ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.fromSingleMk f ⋯ (↑m : ℤ) ⋯ hf)))

Tactic:
exact ⟨f ≫ (R.cochainComplexXIso n n rfl).hom,
    by simpa [R.cochainComplex_d _ _ _ _ rfl rfl,
      ← cancel_mono (R.cochainComplexXIso m m rfl).inv] using hf, by simp [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 : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
⊢ (g ≫ f) ≫ R.cocomplex.d n m = 0

Tactic:
simp [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
X' : C
g : X' ⟶ X
have :
  ∀ (this : HasDerivedCategory C),
    Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R.extMk (g ≫ f) m hm ⋯)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R.extMk (g ≫ f) 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
X' : C
g : X' ⟶ X
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 (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R.extMk (g ≫ f) m hm ⋯))
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R.extMk (g ≫ f) 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
X' : C
g : X' ⟶ X
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 : ℤ))
    (ShiftedHom.comp (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) ⋯ (↑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
        (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 (g ≫ 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))
        ⋯)
      ⋯)
⊢ 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 (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R.extMk (g ≫ f) m hm ⋯))

Tactic:
simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.Ext.mk₀_hom, Int.cast_ofNat_Int, CategoryTheory.InjectiveResolution.extMk, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.comp_hom