awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯
this : Injective.{v', u'} (ShortComplex.X₂ (S.map F))
⊢ S.ShortExact

Tactic:
have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.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 : 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) ⋯
this : Injective.{v', u'} (ShortComplex.X₂ (S.map F))
hS : S.ShortExact
x₁ : Ext.{w, v, u} X S.X₁ (n + 1)
⊢ x₁.comp (Ext.mk₀ S.f) ⋯ = 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 : 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) ⋯
this : Injective.{v', u'} (ShortComplex.X₂ (S.map F))
hS : S.ShortExact
y₁ : Ext.{w', v', u'} (F.obj X) (F.obj S.X₁) (n + 1)
⊢ Eq (α := Ext.{w', v', u'} (F.obj X) (ShortComplex.X₂ (S.map F)) (n + 1))
    (y₁.comp (Ext.mk₀ (ShortComplex.f (S.map F))) ⋯) 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 : 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) ⋯
this : Injective.{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 X S.X₂ n) (F.mapExtAddHom X S.X₃ n) (F.mapExtAddHom X S.X₁ (n + 1))
      (by cat_disch) (by cat_disch)
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' X hS n (n + 1) rfl))
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' (F.obj X) (hS.map F) n (n + 1) rfl))
      (hn _).surjective (hn _)
      (fun x₁ ↦ Ext.covariant_sequence_exact₁ _ hS x₁ (by subsingleton) rfl)
      (fun y₁ ↦ Ext.covariant_sequence_exact₁ _ (hS.map F) y₁ (by subsingleton) rfl)

Premises used: CategoryTheory.ShortComplex.ShortExact.map, CategoryTheory.ShortComplex.X₁, AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', CategoryTheory.ShortComplex.ab_exact_iff_function_exact, CategoryTheory.Functor.mapExtAddHom, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁, HAdd.hAdd, Function.Bijective.surjective, Iff.mp, OfNat.ofNat, CategoryTheory.ShortComplex.X₃, CategoryTheory.Functor.obj, rfl, 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 : EnoughInjectives.{v, u} C
inst_12 : F.PreservesInjectiveObjects
X Y : C
n : ℕ
zero :
  ∀ (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)
succ :
  ∀ (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),
    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 Y with
  | zero => simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩
  | succ n hn =>
    let I : InjectivePresentation Y := Classical.arbitrary _
    let S := ShortComplex.mk _ _ (cokernel.condition I.f)
    have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective
    have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.f }
    exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
      (F.mapExtAddHom X S.X₂ n) (F.mapExtAddHom X S.X₃ n) (F.mapExtAddHom X S.X₁ (n + 1))
      (by cat_disch) (by cat_disch)
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' X hS n (n + 1) rfl))
      ((ShortComplex.ab_exact_iff_function_exact _).mp
        (Ext.covariant_sequence_exact₃' (F.obj X) (hS.map F) n (n + 1) rfl))
      (hn _).surjective (hn _)
      (fun x₁ ↦ Ext.covariant_sequence_exact₁ _ hS x₁ (by subsingleton) rfl)
      (fun y₁ ↦ Ext.covariant_sequence_exact₁ _ (hS.map F) y₁ (by subsingleton) rfl)

Premises used: CategoryTheory.Abelian.Ext.mapExactFunctor₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
obtain :
  ∀ (X : C) (eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)),
    HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
obtain ⟨X, ⟨eX⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj K) a

Premises used: DerivedCategory.Q, DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
obtain :
  ∀ (Y : C) (eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)),
    HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
obtain ⟨Y, ⟨eY⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj L) b

Premises used: DerivedCategory.Q, DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
Y : C
eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)
simp :
  ∀ (a b : ℤ),
    Small.{w, max u v}
      (Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) a) (Functor.obj Q K))
        (Functor.obj (shiftFunctor (DerivedCategory C) b) (Functor.obj Q L)))
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
simp only [hasSmallLocalizedShiftedHom_iff _ _ Q]

Premises used: DerivedCategory.Q, CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
Y : C
eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)
p q : ℤ
φ :
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) p) (Functor.obj Q K))
    (Functor.obj (shiftFunctor (DerivedCategory C) q) (Functor.obj Q L))
⊢ p + (a - p) = a

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
Y : C
eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)
p q : ℤ
φ :
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) p) (Functor.obj Q K))
    (Functor.obj (shiftFunctor (DerivedCategory C) q) (Functor.obj Q L))
⊢ q + (b - q) = b

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
Y : C
eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)
p q : ℤ
φ₁ φ₂ :
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) p) (Functor.obj Q K))
    (Functor.obj (shiftFunctor (DerivedCategory C) q) (Functor.obj Q L))
h :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (SingleFunctors.functor (singleFunctors C) (a - p)) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (b - q)) Y))
    ((fun
          (φ :
            Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) p) (Functor.obj Q K))
              (Functor.obj (shiftFunctor (DerivedCategory C) q) (Functor.obj Q L))) ↦
        (NatTrans.app (Iso.inv (SingleFunctors.shiftIso (singleFunctors C) p (a - p) a ⋯)) X ≫
            Functor.map (shiftFunctor (DerivedCategory C) p) eX.inv ≫
              φ ≫
                Functor.map (shiftFunctor (DerivedCategory C) q) eY.hom ≫
                  NatTrans.app (Iso.hom (SingleFunctors.shiftIso (singleFunctors C) q (b - q) b ⋯)) Y :
          Quiver.Hom (V := DerivedCategory C) (Functor.obj (SingleFunctors.functor (singleFunctors C) (a - p)) X)
            (Functor.obj (SingleFunctors.functor (singleFunctors C) (b - q)) Y)))
      φ₁)
    ((fun
          (φ :
            Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) p) (Functor.obj Q K))
              (Functor.obj (shiftFunctor (DerivedCategory C) q) (Functor.obj Q L))) ↦
        (NatTrans.app (Iso.inv (SingleFunctors.shiftIso (singleFunctors C) p (a - p) a ⋯)) X ≫
            Functor.map (shiftFunctor (DerivedCategory C) p) eX.inv ≫
              φ ≫
                Functor.map (shiftFunctor (DerivedCategory C) q) eY.hom ≫
                  NatTrans.app (Iso.hom (SingleFunctors.shiftIso (singleFunctors C) q (b - q) b ⋯)) Y :
          Quiver.Hom (V := DerivedCategory C) (Functor.obj (SingleFunctors.functor (singleFunctors C) (a - p)) X)
            (Functor.obj (SingleFunctors.functor (singleFunctors C) (b - q)) Y)))
      φ₂)
⊢ φ₁ = φ₂

Tactic:
simpa [cancel_epi, cancel_mono] using h

Premises used: CategoryTheory.cancel_mono, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
a b : ℤ
inst_3 : K.IsGE a
inst_4 : K.IsLE a
inst_5 : L.IsGE b
inst_6 : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_7 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Iso (C := DerivedCategory C) (Functor.obj Q K) (Functor.obj (singleFunctor C a) X)
Y : C
eY : Iso (C := DerivedCategory C) (Functor.obj Q L) (Functor.obj (singleFunctor C b) Y)
⊢ ∀ (a b : ℤ),
    Small.{w, max u v}
      (Quiver.Hom (V := DerivedCategory C) (Functor.obj (shiftFunctor (DerivedCategory C) a) (Functor.obj Q K))
        (Functor.obj (shiftFunctor (DerivedCategory C) b) (Functor.obj Q L)))

Tactic:
exact fun p q ↦ small_of_injective (f := fun φ ↦
    ((singleFunctors C).shiftIso p (a - p) a (by simp)).inv.app X ≫
      eX.inv⟦p⟧' ≫ φ ≫ eY.hom⟦q⟧' ≫
        ((singleFunctors C).shiftIso q (b - q) b (by simp)).hom.app Y)
    (fun φ₁ φ₂ h ↦ by simpa [cancel_epi, cancel_mono] using h)

Premises used: small_of_injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_3 : K.IsGE 0
inst_4 : K.IsLE 0
inst_5 : L.IsGE 0
inst_6 : L.IsLE 0
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE _ _ 0 0

Premises used: CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
rw :
  MorphismProperty.HasLeftCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))
⊢ MorphismProperty.HasLeftCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]

Premises used: HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ MorphismProperty.HasLeftCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
rw :
  MorphismProperty.HasRightCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))
⊢ MorphismProperty.HasRightCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]

Premises used: HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ MorphismProperty.HasRightCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
have :
  ∀
    (φ :
      MorphismProperty.RightFraction (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
        (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
        (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
    (hφ : f = φ.map (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
have ⟨φ, hφ⟩ := Localization.exists_rightFraction Qh (HomotopyCategory.quasiIso C _) f
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
φ :
  MorphismProperty.RightFraction (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
hφ : f = φ.map (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (X' : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (s : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s)
    (g : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
    (hφ :
      f =
        (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) s hs g).map (W :=
          HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
obtain ⟨X', s, hs, g, rfl⟩ := φ.cases

Premises used: CategoryTheory.MorphismProperty.RightFraction.cases, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
s : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
g : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) s hs g).map (W :=
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (s :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X' ⟶
        CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s)
    (g :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X' ⟶
        CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
    (hφ :
      f =
        (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) s hs g).map (W :=
          HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'

Premises used: HomotopyCategory.quotient_obj_surjective, rfl