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 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.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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
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 : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
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 _ _ _ _ _ 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
inst_3 : HasDerivedCategory.{u_1, v, u} C
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 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 ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
      ⋯)

Tactic:
extEquivCohomologyClass_symm_mk_hom _ _

Premises used: CategoryTheory.ProjectiveResolution.extMk, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom
-- 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
p : ℕ
hp : p + 1 = n
simp :
  Membership.mem (γ := AddSubgroup (Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)))
      (coboundaries R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯) ↔
    ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) 0 ↔ ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = 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.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass, Equiv.apply_eq_iff_eq
-- 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
p : ℕ
hp : p + 1 = n
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑p : ℤ)

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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
rw :
  (∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
      ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ↔
    ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f
⊢ Membership.mem (γ := AddSubgroup (Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)))
      (coboundaries R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯) ↔
    ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f

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

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

Tactic:
simpa
-- 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
p : ℕ
hp : p + 1 = n
refine :
  (∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
      ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) →
    ∀ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y)
      (hg :
        ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫
            g =
          (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f),
      R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv ≫ g = f
⊢ (∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
      ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ↔
    ∃ (g : R.complex.X p ⟶ Y), R.complex.d n p ≫ g = f

Tactic:
refine ⟨fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).inv ≫ g, ?_⟩,
    fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).hom ≫ g, by simpa⟩⟩
-- 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
p : ℕ
hp : p + 1 = n
h :
  ∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
    ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
      (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y
hg :
  ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
    (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
rw :
  (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv ≫ g =
    (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
⊢ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv ≫ g = f

Tactic:
rw [← cancel_epi (R.cochainComplexXIso (-n) n rfl).hom]

Premises used: Nat.cast, CategoryTheory.ProjectiveResolution.cochainComplexXIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, Neg.neg, 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
p : ℕ
hp : p + 1 = n
h :
  ∃ (g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y),
    ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
      (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
g : R.cochainComplex.X (-(↑p : ℤ)) ⟶ Y
hg :
  ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv) ≫ g =
    (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f
⊢ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-(↑p : ℤ)) p ⋯).inv ≫ g =
    (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f

Tactic:
simpa [Category.assoc] using hg

Premises used: CategoryTheory.Category.assoc
-- 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 : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
hm : n + 1 = m
obtain :
  ∀ (x : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)),
    ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0),
      Eq.{w + 1} (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf)
        ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          x)
⊢ ∃ (f : R.complex.X n ⟶ Y) (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = α

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

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

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

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

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 m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y
hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0
refine : R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).inv ≫ f = 0
⊢ ∃ (f_1 : R.complex.X n ⟶ Y) (hf_1 : R.complex.d m n ≫ f_1 = 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 R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk f ⋯ (-(↑m : ℤ)) ⋯ hf)))

Tactic:
refine ⟨(R.cochainComplexXIso (-n) n rfl).inv ≫ f, ?_, by simp [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 m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y
hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0
rw :
  (R.cochainComplexXIso (-(↑m : ℤ)) m ⋯).hom ≫ R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).inv ≫ f =
    (R.cochainComplexXIso (-(↑m : ℤ)) m ⋯).hom ≫ 0
⊢ R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).inv ≫ f = 0

Tactic:
rw [← cancel_epi (R.cochainComplexXIso (-m) m rfl).hom]

Premises used: Nat.cast, CategoryTheory.ProjectiveResolution.cochainComplexXIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, Neg.neg, 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 m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-(↑n : ℤ)) ⟶ Y
hf : Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y) (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ f) 0
⊢ (R.cochainComplexXIso (-(↑m : ℤ)) m ⋯).hom ≫ R.complex.d m n ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).inv ≫ f =
    (R.cochainComplexXIso (-(↑m : ℤ)) m ⋯).hom ≫ 0

Tactic:
simpa [R.cochainComplex_d _ _ _ _ rfl rfl] using hf

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_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
⊢ R.complex.d m n ≫ f ≫ g = 0

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

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

Tactic:
ext
-- 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
Y' : C
g : Y ⟶ Y'
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.comp
        (ShiftedHom.mk₀ 0 ⋯
          (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
            inv (Functor.map DerivedCategory.Q R.π')))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                  R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
              (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
        ⋯)
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g)) ⋯)
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y') (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y'))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')) ⋯)
      ⋯)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (Ext.hom (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯)) (Ext.hom (R.extMk (f ≫ g) m hm ⋯))

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

Premises used: CategoryTheory.ProjectiveResolution.extMk, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, Int.cast_ofNat_Int, CategoryTheory.Abelian.Ext.comp_hom
-- 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
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ 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
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ HAdd.hAdd (α := ℤ) 0 (↑n : ℤ) + 0 = (↑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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ HAdd.hAdd (α := ℤ) 0 0 + (↑n : ℤ) = (↑n : ℤ)

Tactic:
simp