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 m : ℕ
hm : n + 1 = m
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)
have 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))
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 m : ℕ
hm : n + 1 = m
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))
have 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 sorry (↑m : ℤ) sorry hf)))
Tactic: obtain ⟨f, hf, rfl⟩ := Cocycle.fromSingleMk_surjective x n (by simp) m (by lia)
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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
⊢ 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 ⋯)
have 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) sorry) (R.extMk (g ≫ f) m hm sorry)
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 : ℕ
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
⊢ 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 ⋯)
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 (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) sorry)) (Ext.hom (R.extMk (g ≫ f) m hm sorry))
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 : 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
⊢ 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 ⋯))
have 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 sorry (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 sorry).inv) sorry (↑m : ℤ) sorry sorry))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 sorry
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        sorry)
      sorry)
    sorry)
  (ShiftedHom.comp (ShiftedHom.mk₀ 0 sorry (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 sorry).inv) sorry (↑m : ℤ) sorry sorry))
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 sorry
        (inv (Functor.map DerivedCategory.Q R.ι') ≫
          NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
      sorry)
    sorry)
Tactic: simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom, Category.assoc]
-- 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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y' n) (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) ⋯) (R'.extMk (f ≫ φ.hom.f n) m hm ⋯)
have 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) sorry) (R'.extMk (f ≫ φ.hom.f n) m hm sorry)
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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
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 ≫ φ.hom.f n) m hm ⋯)
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 (Ext.comp (R.extMk f m hm hf) (Ext.mk₀ g) sorry)) (Ext.hom (R'.extMk (f ≫ φ.hom.f n) m hm sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Ext (hypothesis)
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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this : HasDerivedCategory C
⊢ 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 ≫ φ.hom.f n) m hm ⋯))
have this₁ : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n sorry).inv =
  (f ≫ (R.cochainComplexXIso (↑n : ℤ) n sorry).inv) ≫ φ.hom'.f (↑n : ℤ)
Tactic: have : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso n n (by lia)).inv =
      (f ≫ (R.cochainComplexXIso n n (by lia)).inv) ≫ φ.hom'.f n := by
    simp [φ.hom'_f n n 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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ 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 ≫ φ.hom.f n) m hm ⋯))
have 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 sorry (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 sorry).inv) sorry (↑m : ℤ) sorry sorry))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 sorry
          (inv (Functor.map DerivedCategory.Q R.ι') ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y))
        sorry)
      sorry)
    (ShiftedHom.mk₀ (↑0 : ℤ) Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g)) sorry)
  (ShiftedHom.comp (ShiftedHom.mk₀ 0 sorry (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 sorry).inv) ≫ φ.hom'.f (↑n : ℤ)) sorry (↑m : ℤ) sorry sorry))
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 sorry
        (inv (Functor.map DerivedCategory.Q R'.ι') ≫
          NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
      sorry)
    sorry)
Tactic: simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, this]
-- 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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp (b := (↑n : ℤ))
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp (b := 0)
        (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) ≫
            Functor.map (DerivedCategory.singleFunctor C 0) g))
        ⋯)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X))
      (ShiftedHom.comp (b := 0)
        (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 ⋯
          (Functor.map DerivedCategory.Q φ.hom' ≫
            inv (Functor.map DerivedCategory.Q R'.ι') ≫
              NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)
have h : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
  ((inv (Functor.map DerivedCategory.Q R.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y) ≫
    Functor.map (DerivedCategory.singleFunctor C 0) g)
  (Functor.map DerivedCategory.Q φ.hom' ≫
    inv (Functor.map DerivedCategory.Q R'.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
Tactic: congr 3
-- 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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y) ≫
      Functor.map (DerivedCategory.singleFunctor C 0) g)
    (Functor.map DerivedCategory.Q φ.hom' ≫
      inv (Functor.map DerivedCategory.Q R'.ι') ≫ NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
have h : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
  ((inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g) ≫
    NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
  ((Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι')) ≫
    NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
Tactic: rw [Category.assoc, ← NatTrans.naturality, ← Category.assoc, ← Category.assoc]
-- 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
Y' : C
R' : InjectiveResolution.{v, u} Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this_1 : HasDerivedCategory C
this :
  (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n : ℤ) n ⋯).inv =
    (f ≫ (R.cochainComplexXIso (↑n : ℤ) n ⋯).inv) ≫ φ.hom'.f (↑n : ℤ)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y'))
    ((inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
    ((Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι')) ≫
      NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y')
have h : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q R.cochainComplex)
    (Functor.obj (singleFunctor C 0 ⋙ DerivedCategory.Q) Y'))
  (inv (Functor.map DerivedCategory.Q R.ι') ≫ Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g)
  (Functor.map DerivedCategory.Q φ.hom' ≫ inv (Functor.map DerivedCategory.Q R'.ι'))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
⊢ Injective.{v, u} (R.cochainComplex.X n)
have pos : ∀ (hn : 0 ≤ n), Injective.{v, u} (R.cochainComplex.X n)
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
pos : ∀ (hn : 0 ≤ n), Injective.{v, u} (R.cochainComplex.X n)
⊢ Injective.{v, u} (R.cochainComplex.X n)
have neg : ∀ (hn : ¬0 ≤ n), Injective.{v, u} (R.cochainComplex.X n)
Tactic: by_cases hn : 0 ≤ n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
n : ℤ
hn : 0 ≤ n
⊢ Injective.{v, u} (R.cochainComplex.X n)
have pos : ∀ (k : ℕ) (hn : LE.le (α := ℤ) 0 (↑k : ℤ)), Injective.{v, u} (R.cochainComplex.X (↑k : ℤ))
Tactic: obtain ⟨k, rfl⟩ := Int.eq_ofNat_of_zero_le hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ R.ι'.f 0 =
    Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv
have dsimp : Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
  (HomologicalComplex.Hom.f (Iso.inv (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1))
      0 ≫
    HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat) 0)
  (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
    R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)
Tactic: dsimp [ι']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
    (HomologicalComplex.Hom.f
        (Iso.inv (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1)) 0 ≫
      HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat) 0)
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)
have rw : Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
  (CategoryStruct.comp (Y :=
    HomologicalComplex.X.{v, u, 0}
      (HomologicalComplex.extend (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
        ComplexShape.embeddingUpNat)
      0)
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X) ≫
        Iso.inv
          (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
            ComplexShape.embeddingUpNat ι'._proof_1))
    (Iso.hom
        (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
          ComplexShape.embeddingUpNat sorry) ≫
      R.ι.f 0 ≫ Iso.inv (HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat sorry)))
  (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
    R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)
Tactic: rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_inv_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ R.cochainComplex.IsLE 0
have simp : HomologicalComplex.IsSupported.{0, 0, v, u} (Functor.obj (CochainComplex.singleFunctor C 0) X)
  (ComplexShape.embeddingUpIntLE 0)
Tactic: simp only [← HomologicalComplex.isSupported_iff_of_quasiIso R.ι']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ Eq (α :=
    { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.X₁ ⟶
      I.cocomplex.X 1)
    ({ X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.f ≫
      descFZero f I J ≫ I.cocomplex.d 0 1)
    0
have dsimp : Eq (α := Z ⟶ I.cocomplex.X 1) (J.ι.f 0 ≫ descFZero f I J ≫ I.cocomplex.d 0 1) 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ Eq (α := Z ⟶ I.cocomplex.X 1) (J.ι.f 0 ≫ descFZero f I J ≫ I.cocomplex.d 0 1) 0
have simp : Eq (α := Z ⟶ I.cocomplex.X 1)
  (CategoryStruct.comp (Y := I.cocomplex.X 0)
      (CategoryStruct.comp (Y := J.cocomplex.X 0) (J.ι.f 0) (factorThru (f ≫ I.ι.f 0) (J.ι.f 0))) (I.cocomplex.d 0 1) :
    Z ⟶ I.cocomplex.X 1)
  (0 :
    { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := sorry : ShortComplex.{v, u} C }.X₁ ⟶
      I.cocomplex.X 1)
Tactic: simp only [← assoc, descFZero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ J.ι ≫ desc f I J = Functor.map (CochainComplex.single₀ C) f ≫ I.ι
have hfg : Eq (α :=
  HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) Z) 0 ⟶
    I.cocomplex.X 0)
  ((J.ι ≫ desc f I J).f 0) ((Functor.map (CochainComplex.single₀ C) f ≫ I.ι).f 0)
Tactic: ext