awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
      (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X) (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
          HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
          (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
        (Functor.obj (CochainComplex.singleFunctor C 0) X))
      (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X) :
        Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
          (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X)
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
            (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
              HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
              (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
            (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.map
            (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
              HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
              (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
            (Functor.map (CochainComplex.singleFunctor C 0) f) ≫
          Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y) :
        Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
            (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
              HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
              (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
            (Functor.obj (CochainComplex.singleFunctor C 0) X))
          (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y)))
    (Functor.map (CochainComplex.singleFunctor D 0) (F.map f))

Tactic:
simpa only [Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor,
    Functor.mapCochainComplexSingleFunctor, Iso.app_inv, Iso.app_hom] using NatIso.naturality_1 _ f

Premises used: CategoryTheory.Iso.app_inv, CategoryTheory.NatIso.naturality_1, CategoryTheory.Functor.mapCochainComplexSingleFunctor, CategoryTheory.Iso.app_hom, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
h :
  ∀ (x : Ext.{w, v, u} X Y 0),
    Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0) (mapExactFunctor F x)
      (Function.comp (β := F.obj X ⟶ F.obj Y)
        (⇑(Equiv.symm homEquiv₀) : (a : F.obj X ⟶ F.obj Y) → Ext (F.obj X) (F.obj Y) 0)
        (F.map ∘ (⇑homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y)) x)
⊢ Eq (α := (f : Ext.{w, v, u} X Y 0) → Ext.{w', v', u'} (F.obj X) (F.obj Y) 0) (mapExactFunctor F)
    (Function.comp (β := F.obj X ⟶ F.obj Y)
      (⇑(Equiv.symm homEquiv₀) : (a : F.obj X ⟶ F.obj Y) → Ext (F.obj X) (F.obj Y) 0)
      (F.map ∘ (⇑homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y)))

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
x : Ext.{w, v, u} X Y 0
h :
  ∀ (y : X ⟶ Y) (hy : mk₀ y = x),
    Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0) (mapExactFunctor F x)
      (Function.comp (β := F.obj X ⟶ F.obj Y)
        (⇑(Equiv.symm homEquiv₀) : (a : F.obj X ⟶ F.obj Y) → Ext (F.obj X) (F.obj Y) 0)
        (F.map ∘ (⇑homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y)) x)
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0) (mapExactFunctor F x)
    (Function.comp (β := F.obj X ⟶ F.obj Y)
      (⇑(Equiv.symm homEquiv₀) : (a : F.obj X ⟶ F.obj Y) → Ext (F.obj X) (F.obj Y) 0)
      (F.map ∘ (⇑homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y)) x)

Tactic:
rcases (Ext.mk₀_bijective X Y).2 x with ⟨y, hy⟩

Premises used: And.right, CategoryTheory.Abelian.Ext.mk₀_bijective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
x : Ext.{w, v, u} X Y 0
y : X ⟶ Y
hy : mk₀ y = x
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0) (mapExactFunctor F x)
    (Function.comp (β := F.obj X ⟶ F.obj Y)
      (⇑(Equiv.symm homEquiv₀) : (a : F.obj X ⟶ F.obj Y) → Ext (F.obj X) (F.obj Y) 0)
      (F.map ∘ (⇑homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y)) x)

Tactic:
simp [← hy, Ext.mapExactFunctor_mk₀, Ext.homEquiv₀]

Premises used: CategoryTheory.Abelian.Ext.homEquiv₀, CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y Z : C
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
⊢ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑c : ℤ)

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory D) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₁)) (↑1 : ℤ))
    (hom (mapExactFunctor.{w, w', u, u', v, v'} F hS.extClass)) (hom (ShortComplex.ShortExact.extClass ⋯))
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj S.X₃) (F.obj S.X₁) 1) (mapExactFunctor.{w, w', u, u', v, v'} F hS.extClass)
    (ShortComplex.ShortExact.extClass ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory D) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₁)) (↑1 : ℤ))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := DerivedCategory C) (DerivedCategory.singleFunctor C 0) F.mapDerivedCategory) S.X₃)
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        Functor.map (shiftFunctor (DerivedCategory D) (A := ℤ) (↑1 : ℤ))
          (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))
    (hom (ShortComplex.ShortExact.extClass ⋯))
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory D) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₁)) (↑1 : ℤ))
    (hom (mapExactFunctor.{w, w', u, u', v, v'} F hS.extClass)) (hom (ShortComplex.ShortExact.extClass ⋯))

Tactic:
rw [Ext.mapExactFunctor_hom, hS.extClass_hom]

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory D) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₁)) (↑1 : ℤ))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := DerivedCategory C) (DerivedCategory.singleFunctor C 0) F.mapDerivedCategory) S.X₃)
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        Functor.map (shiftFunctor (DerivedCategory D) (A := ℤ) (↑1 : ℤ))
          (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))
    (hom (ShortComplex.ShortExact.extClass ⋯))

Tactic:
(hS.mapShiftedHom_singleδ' F).trans (hS.map_of_exact F).extClass_hom.symm

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ', Eq.symm, CategoryTheory.ShortComplex.ShortExact.map_of_exact, Eq.trans
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory D) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (DerivedCategory.singleFunctor D 0) (F.obj S.X₁)) (↑1 : ℤ))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := DerivedCategory C) (DerivedCategory.singleFunctor C 0) F.mapDerivedCategory) S.X₃)
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        Functor.map (shiftFunctor (DerivedCategory D) (A := ℤ) (↑1 : ℤ))
          (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))
    (hom (ShortComplex.ShortExact.extClass ⋯))

Tactic:
exact (hS.mapShiftedHom_singleδ' F).trans (hS.map_of_exact F).extClass_hom.symm

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ', Eq.symm, CategoryTheory.ShortComplex.ShortExact.map_of_exact, Eq.trans
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y X : C
⊢ Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y 0) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0)
    (⇑(F.mapExtAddHom X Y 0) : (a : Ext X Y 0) → Ext (F.obj X) (F.obj Y) 0)

Tactic:
simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
X : C
P : ProjectivePresentation.{v, u} X := Classical.arbitrary (ProjectivePresentation.{v, u} X)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := Limits.kernel P.f) (kernel.ι P.f) P.f ⋯
⊢ Projective.{v', u'} (ShortComplex.X₂ (S.map F))

Tactic:
have : Projective (S.map F).X₂ := Functor.PreservesProjectiveObjects.projective_obj P.projective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
X : C
P : ProjectivePresentation.{v, u} X := Classical.arbitrary (ProjectivePresentation.{v, u} X)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := Limits.kernel P.f) (kernel.ι P.f) P.f ⋯
this : Projective.{v', u'} (ShortComplex.X₂ (S.map F))
⊢ S.ShortExact

Tactic:
have hS : S.ShortExact := { exact := ShortComplex.exact_kernel P.f }
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
X : C
P : ProjectivePresentation.{v, u} X := Classical.arbitrary (ProjectivePresentation.{v, u} X)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := Limits.kernel P.f) (kernel.ι P.f) P.f ⋯
this : Projective.{v', u'} (ShortComplex.X₂ (S.map F))
hS : S.ShortExact
x₃ : Ext.{w, v, u} S.X₃ Y (n + 1)
⊢ Ext.comp (Ext.mk₀ S.g) x₃ ⋯ = 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
X : C
P : ProjectivePresentation.{v, u} X := Classical.arbitrary (ProjectivePresentation.{v, u} X)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := Limits.kernel P.f) (kernel.ι P.f) P.f ⋯
this : Projective.{v', u'} (ShortComplex.X₂ (S.map F))
hS : S.ShortExact
y₃ : Ext.{w', v', u'} (F.obj S.X₃) (F.obj Y) (n + 1)
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (ShortComplex.X₂ (S.map F)) (F.obj Y) (n + 1))
    (Ext.comp (Ext.mk₀ (ShortComplex.g (S.map F))) y₃ ⋯) 0

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
X : C
P : ProjectivePresentation.{v, u} X := Classical.arbitrary (ProjectivePresentation.{v, u} X)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := Limits.kernel P.f) (kernel.ι P.f) P.f ⋯
this : Projective.{v', u'} (ShortComplex.X₂ (S.map F))
hS : S.ShortExact
⊢ Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y (n + 1)) (β :=
    Ext.{w', v', u'} (F.obj X) (F.obj Y) (n + 1))
    (⇑(F.mapExtAddHom X Y (n + 1)) : (a : Ext X Y (n + 1)) → Ext (F.obj X) (F.obj Y) (n + 1))

Tactic:
exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
      (F.mapExtAddHom S.X₂ Y n) (F.mapExtAddHom S.X₁ Y n) (F.mapExtAddHom S.X₃ Y (n + 1))
      (by cat_disch) (by cat_disch)
      ((ShortComplex.ab_exact_iff_function_exact _).1
        (Ext.contravariant_sequence_exact₁' hS Y n (n + 1) (add_comm 1 n)))
      ((ShortComplex.ab_exact_iff_function_exact _).1
        (Ext.contravariant_sequence_exact₁' (hS.map F) (F.obj Y) n (n + 1) (add_comm 1 n)))
      (hn _).surjective (hn _)
      (fun x₃ ↦ Ext.contravariant_sequence_exact₃ hS _ x₃ (by subsingleton) (add_comm 1 n))
      (fun y₃ ↦ Ext.contravariant_sequence_exact₃ (hS.map F) _ y₃ (by subsingleton) (add_comm 1 n))

Premises used: CategoryTheory.ShortComplex.ShortExact.map, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', CategoryTheory.ShortComplex.X₁, AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, CategoryTheory.Functor.mapExtAddHom, add_comm, HAdd.hAdd, Function.Bijective.surjective, Iff.mp, OfNat.ofNat, CategoryTheory.ShortComplex.X₃, CategoryTheory.Functor.obj, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughProjectives.{v, u} C
inst_12 : F.PreservesProjectiveObjects
X Y : C
n : ℕ
zero :
  ∀ (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y 0) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0)
      (⇑(F.mapExtAddHom X Y 0) : (a : Ext X Y 0) → Ext (F.obj X) (F.obj Y) 0)
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (X : C),
        Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
          (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n))
    (X : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y (n + 1)) (β :=
      Ext.{w', v', u'} (F.obj X) (F.obj Y) (n + 1))
      (⇑(F.mapExtAddHom X Y (n + 1)) : (a : Ext X Y (n + 1)) → Ext (F.obj X) (F.obj Y) (n + 1))
⊢ Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
    (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)

Tactic:
induction n generalizing X with
  | zero => simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩
  | succ n hn =>
    let P : ProjectivePresentation X := Classical.arbitrary _
    let S := ShortComplex.mk _ _ (kernel.condition P.f)
    have : Projective (S.map F).X₂ := Functor.PreservesProjectiveObjects.projective_obj P.projective
    have hS : S.ShortExact := { exact := ShortComplex.exact_kernel P.f }
    exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
      (F.mapExtAddHom S.X₂ Y n) (F.mapExtAddHom S.X₁ Y n) (F.mapExtAddHom S.X₃ Y (n + 1))
      (by cat_disch) (by cat_disch)
      ((ShortComplex.ab_exact_iff_function_exact _).1
        (Ext.contravariant_sequence_exact₁' hS Y n (n + 1) (add_comm 1 n)))
      ((ShortComplex.ab_exact_iff_function_exact _).1
        (Ext.contravariant_sequence_exact₁' (hS.map F) (F.obj Y) n (n + 1) (add_comm 1 n)))
      (hn _).surjective (hn _)
      (fun x₃ ↦ Ext.contravariant_sequence_exact₃ hS _ x₃ (by subsingleton) (add_comm 1 n))
      (fun y₃ ↦ Ext.contravariant_sequence_exact₃ (hS.map F) _ y₃ (by subsingleton) (add_comm 1 n))

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughInjectives.{v, u} C
inst_12 : F.PreservesInjectiveObjects
X Y : C
⊢ Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y 0) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0)
    (⇑(F.mapExtAddHom X Y 0) : (a : Ext X Y 0) → Ext (F.obj X) (F.obj Y) 0)

Tactic:
simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : F.Full
inst_8 : F.Faithful
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
inst_11 : EnoughInjectives.{v, u} C
inst_12 : F.PreservesInjectiveObjects
X : C
n : ℕ
hn :
  ∀ (Y : C),
    Function.Bijective.{w + 1, w' + 1} (α := Ext.{w, v, u} X Y n) (β := Ext.{w', v', u'} (F.obj X) (F.obj Y) n)
      (⇑(F.mapExtAddHom X Y n) : (a : Ext X Y n) → Ext (F.obj X) (F.obj Y) n)
Y : C
I : InjectivePresentation.{v, u} Y := Classical.arbitrary (InjectivePresentation.{v, u} Y)
S : ShortComplex.{v, u} C := ShortComplex.mk (X₃ := cokernel I.f) I.f (cokernel.π I.f) ⋯
⊢ Injective.{v', u'} (ShortComplex.X₂ (S.map F))

Tactic:
have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective