awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
mp :
  (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
have mpr : (∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))) →
  ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
have mpr : ∀ (hab : a ≤ b),
  Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
Tactic: obtain hab | hab := le_or_gt a b
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
mpr :
  ∀ (hab : a ≤ b),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
have mpr₁ : ∀ (hab : b < a),
  Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
Tactic: obtain hab | hab := le_or_gt a b
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
have mpr : Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) (b - a)) (Functor.obj (singleFunctor C 0) Y)) ≃
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
Tactic: refine (small_congr ?_).1 (h X Y (b - a) (by simpa))
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
have mpr : Subsingleton.{w' + 1}
  (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
Tactic: suffices Subsingleton ((Q.obj ((CochainComplex.singleFunctor C 0).obj X))⟦a⟧ ⟶
          (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))⟦b⟧) from inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
⊢ Subsingleton.{w' + 1}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
have mpr : ∀
  (a_1 b_1 :
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))),
  a_1 = b_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
⊢ x = y
have mpr : Eq (α :=
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙ Q) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b ⋙ Q)
      (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
  (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
    x ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
  (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
    y ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
Tactic: rw [← cancel_mono ((Q.commShiftIso b).inv.app _),
        ← cancel_epi ((Q.commShiftIso a).hom.app _)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) X))
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      x ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      y ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
have this : CochainComplex.IsStrictlyLE.{v, u}
  (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X)) (-a)
Tactic: have : (((CochainComplex.singleFunctor C 0).obj X)⟦a⟧).IsStrictlyLE (-a) :=
        CochainComplex.isStrictlyLE_shift _ 0 _ _ (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
this :
  CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) X))
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      x ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      y ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
have this₁ : CochainComplex.IsStrictlyGE.{v, u}
  (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b) (Functor.obj (CochainComplex.singleFunctor C 0) Y)) (-b)
Tactic: have : (((CochainComplex.singleFunctor C 0).obj Y)⟦b⟧).IsStrictlyGE (-b) :=
        CochainComplex.isStrictlyGE_shift _ 0 _ _ (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ HasExt.{w, v, u} C
have rw : ∀ (X Y : C) (n : ℤ),
  0 ≤ n →
    Small.{w, w}
      (Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
Tactic: rw [hasExt_iff.{w}]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
a b : ℤ
inst_3 : HasDerivedCategory.{w', v, u} C
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X)
      (Functor.obj (singleFunctor C b) Y))
have this : ∀ (a b : ℤ),
  Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a) (Functor.obj (singleFunctor C 0) X))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b) (Functor.obj (singleFunctor C 0) Y)))
Tactic: have (a b : ℤ) :
      Small.{w} (((singleFunctor C 0).obj X)⟦a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦b⟧) :=
    (hasSmallLocalizedShiftedHom_iff.{w}
      (W := (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))) (M := ℤ)
      (X := (CochainComplex.singleFunctor C 0).obj X)
      (Y := (CochainComplex.singleFunctor C 0).obj Y) Q).1 inferInstance a b
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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 Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z 0
γ : Ext.{w, v, u} Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃
have h : a₁ + 0 + a₃ = a₁₃
Tactic: apply comp_assoc
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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 Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂
have h : a₁ + a₂ + 0 = a₁₂
Tactic: apply comp_assoc
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Z 0) (comp (mk₀ f) (mk₀ g) ⋯) (mk₀ (f ≫ g))
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
    (↑0 : ℤ))
  (hom (comp (mk₀ f) (mk₀ g) sorry)) (hom (mk₀ (f ≫ g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext.{w, v, u} Z T n
⊢ comp (mk₀ f) (comp (mk₀ g) α ⋯) ⋯ = comp (mk₀ (f ≫ g)) α ⋯
have h : HAdd.hAdd (α := ℕ) 0 0 + n = n
Tactic: rw [← mk₀_comp_mk₀, comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀
have have : ∀ (h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)),
  Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀
Tactic: have h : (singleFunctor C 0).FullyFaithful := Functor.FullyFaithful.ofFullyFaithful _
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
⊢ e.toFun = mk₀
have h₁ : ∀ (f : X ⟶ Y), e.toFun f = mk₀ f
Tactic: ext f : 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
⊢ e.toFun f = mk₀ f
have h₁ : Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
  ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
      (ShiftedHom.mk₀ 0 sorry (Functor.map (singleFunctor C 0) f)) :
    Ext.{w, v, u} X Y 0)
  (mk₀ f : Ext.{w, v, u} X Y 0)
Tactic: dsimp [e]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
        (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f)) :
      Ext.{w, v, u} X Y 0)
    (mk₀ f : Ext.{w, v, u} X Y 0)
have h₁ : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
    (↑0 : ℤ))
  ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
      ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
        (ShiftedHom.mk₀ 0 sorry (Functor.map (singleFunctor C 0) f))) :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
  ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ)) (mk₀ f) :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
Tactic: apply homEquiv.injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
          (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f))) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        (mk₀ f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
have h₁ : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
    (↑0 : ℤ))
  (ShiftedHom.mk₀ 0 sorry (Functor.map (singleFunctor C 0) f))
  ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ)) (mk₀ f))
Tactic: apply (Equiv.apply_symm_apply _ _).trans