awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
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
⊢ 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)))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
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
⊢ 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)
have 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)
Tactic: rcases (Ext.mk₀_bijective X Y).2 x with ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
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.{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 ⋯)
have 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 sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
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 : ℤ))
    (hom (mapExactFunctor.{w, w', u, u', v, v'} F hS.extClass)) (hom (ShortComplex.ShortExact.extClass ⋯))
have 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 sorry))
Tactic: rw [Ext.mapExactFunctor_hom, hS.extClass_hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (hypothesis)
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 ⋯
⊢ 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))
have this : Projective.{v', u'} (ShortComplex.X₂ (S.map F))
Tactic: have : Projective (S.map F).X₂ := Functor.PreservesProjectiveObjects.projective_obj P.projective
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (hypothesis)
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))
⊢ 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))
have hS : S.ShortExact
Tactic: have hS : S.ShortExact := { exact := ShortComplex.exact_kernel P.f }
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (goal)
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 : ℕ
⊢ 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)
have 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)
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))
Cleared hypotheses: X, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (goal)
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)
⊢ 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)
have 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))
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))
Cleared hypotheses: X, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (hypothesis)
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) ⋯
⊢ 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))
have this : Injective.{v', u'} (ShortComplex.X₂ (S.map F))
Tactic: have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (hypothesis)
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))
⊢ 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))
have hS : S.ShortExact
Tactic: have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.f }
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (goal)
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 : ℕ
⊢ 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)
have 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)
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)
Cleared hypotheses: Y, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective (goal)
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)
⊢ 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)
have 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))
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)
Cleared hypotheses: Y, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure (goal)
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
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
have 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
Tactic: obtain ⟨X, ⟨eX⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj K) a
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure (goal)
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)
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
have 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
Tactic: obtain ⟨Y, ⟨eY⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj L) b
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure (goal)
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)
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
have 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)))
Tactic: simp only [hasSmallLocalizedShiftedHom_iff _ _ Q]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ℤ))
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
have rw : MorphismProperty.HasLeftCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
  (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))
Tactic: rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ℤ))
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
have rw : MorphismProperty.HasRightCalculusOfFractions (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
  (ObjectProperty.trW (HomotopyCategory.subcategoryAcyclic C))
Tactic: rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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' : 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
have 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 sorry),
  ∃ (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