awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
h₂ : section_ π ≫ g = 0
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q g) 0
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q (section_ π ≫ g)) 0
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have rw₂ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q L))
  (CategoryTheory.Functor.map Q 0) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
h₂ : section_ π ≫ g = 0
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q g) 0
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q (section_ π ≫ g)) 0
rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q 0) 0
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have rw₃ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q L))
  0 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ e = 0
have a : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
    (↑(n + 1) : ℤ))
  ((homEquiv :
        (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
      e :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
      (↑(n + 1) : ℤ))
  ((homEquiv :
        (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
      0 :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
      (↑(n + 1) : ℤ))
Tactic: apply homEquiv.injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))
have a : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
    (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
  ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        e ≫
      NatTrans.app
        (Iso.hom
          (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 0
            sorry))
        Y :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
  (0 :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
Tactic: simp only [← cancel_mono (((singleFunctors C).shiftIso (n + 1) (-(n + 1)) 0
    (by lia)).hom.app _), zero_hom, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt.{w, v, u} C
have this₁ : HasExt C
Tactic: have := hasExt_of_hasDerivedCategory C
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)
have zero : Small.{w, v} (X ⟶ Y)
Tactic: rw [small_congr Ext.homEquiv₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₁ := kernel.{v, u} (X := Projective.over.{v, u} X) (Projective.π X)) (kernel.ι (Projective.π X))
    (Projective.π X) ⋯
⊢ Small.{w, max u v} (Ext X Y (n + 1))
have hS : S.ShortExact
Tactic: have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₁ := kernel.{v, u} (X := Projective.over.{v, u} X) (Projective.π X)) (kernel.ι (Projective.π X))
    (Projective.π X) ⋯
hS : S.ShortExact
⊢ Small.{w, max u v} (Ext X Y (n + 1))
have this₁ : Function.Surjective (α := Ext S.X₁ Y n) (β := Ext S.X₃ Y (n + 1))
  (⇑(Ext.precomp hS.extClass Y sorry) : (a : Ext S.X₁ Y n) → Ext S.X₃ Y (n + 1))
Tactic: have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
      Ext.contravariant_sequence_exact₃ hS Y x₃
        (Ext.eq_zero_of_projective _) (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
⊢ Small.{w, max u v} (Ext X Y n)
have zero : ∀ (X Y : C), Small.{w, max u v} (Ext X Y 0)
Tactic: induction n generalizing X Y with
  | zero =>
    rw [small_congr Ext.homEquiv₀]
    infer_instance
  | succ n hn =>
    let S := ShortComplex.mk _ _ (kernel.condition (Projective.π X))
    have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
    have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
      Ext.contravariant_sequence_exact₃ hS Y x₃
        (Ext.eq_zero_of_projective _) (by lia)
    exact small_of_surjective.{w} this
Cleared hypotheses: X, Y, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
zero : ∀ (X Y : C), Small.{w, max u v} (Ext X Y 0)
⊢ Small.{w, max u v} (Ext X Y n)
have succ : ∀ (n : ℕ) (hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)) (X Y : C), Small.{w, max u v} (Ext X Y (n + 1))
Tactic: induction n generalizing X Y with
  | zero =>
    rw [small_congr Ext.homEquiv₀]
    infer_instance
  | succ n hn =>
    let S := ShortComplex.mk _ _ (kernel.condition (Projective.π X))
    have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
    have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
      Ext.contravariant_sequence_exact₃ hS Y x₃
        (Ext.eq_zero_of_projective _) (by lia)
    exact small_of_surjective.{w} this
Cleared hypotheses: X, Y, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
inst_3 : HasDerivedCategory.{w', v, u} C
X : C
n₀ : ℕ
x : Ext.{w, v, u} X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    (↑(Functor.obj (C := DerivedCategory.{w', v, u} C)
          (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₁ : ℤ))
          (Triangle.obj₁ hS.singleTriangle)) :
      Type w'))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj (C := DerivedCategory.{w', v, u} C)
              (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
                (↑n₀ : ℤ))
              (Triangle.obj₃ hS.singleTriangle))
            (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
              hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯) :
          (a :
              (↑(((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift (↑n₀ : ℤ)).obj
                    hS.singleTriangle.obj₃) :
                Type w')) →
            (↑(((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift (↑n₁ : ℤ)).obj
                  hS.singleTriangle.obj₁) :
              Type w'))
        x.hom :
      (↑(Functor.obj (C := DerivedCategory.{w', v, u} C)
            (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ)
              (↑n₁ : ℤ))
            (Triangle.obj₁ hS.singleTriangle)) :
        Type w'))
    ((x.comp hS.extClass h).hom :
      ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) S.X₁) (↑n₁ : ℤ))
have rw : Eq.{w' + 1} (α :=
  (↑(Functor.obj (C := DerivedCategory.{w', v, u} C)
        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₁ : ℤ))
        (Triangle.obj₁ hS.singleTriangle)) :
    Type w'))
  (x.hom ≫
    Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑n₀ : ℤ)) (Triangle.mor₃ hS.singleTriangle) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) 1 (↑n₀ : ℤ) (↑n₁ : ℤ) sorry))
        (Triangle.obj₁ hS.singleTriangle))
  (x.hom ≫
    Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑n₀ : ℤ)) hS.singleδ ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) (↑1 : ℤ) (↑n₀ : ℤ) (↑n₁ : ℤ) sorry))
        (Functor.obj (singleFunctor C 0) S.X₁))
Tactic: rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Eq.{w + 1} (α := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀) ⟶ AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n₁))
    (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯) ≫ AddCommGrpCat.ofHom (postcomp hS.extClass X h)) 0
have hf : ∀ (x : (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀)) : Type w)),
  Eq (α := (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n₁)) : Type w))
    ((AddCommGrpCat.Hom.hom
            (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry) ≫ AddCommGrpCat.ofHom (postcomp hS.extClass X h)) :
          (a : (↑(AddCommGrpCat.of (Ext X S.X₂ n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext X S.X₁ n₁)) : Type w))
        x :
      (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n₁)) : Type w))
    ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of (Ext X S.X₂ n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext X S.X₁ n₁)) : Type w))
        x :
      (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n₁)) : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯))
      (AddCommGrpCat.ofHom (postcomp hS.extClass X h)) ⋯).Exact
have this₁ : (ShortComplex.mk (X₁ :=
    Functor.obj (C := DerivedCategory C)
      (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
      (Triangle.obj₂ hS.singleTriangle))
    (Functor.map
      (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
      (Triangle.mor₂ hS.singleTriangle))
    (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
      hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) sorry)
    sorry).Exact
Tactic: have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₃ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk (X₁ :=
      Functor.obj (C := DerivedCategory C)
        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₂ hS.singleTriangle))
      (Functor.map
        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.mor₂ hS.singleTriangle))
      (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
        hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
      ⋯).Exact
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯))
      (AddCommGrpCat.ofHom (postcomp hS.extClass X h)) ⋯).Exact
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Eq.{w + 1} (α := AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀) ⟶ AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₁))
    (AddCommGrpCat.ofHom (postcomp hS.extClass X h) ≫ AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X ⋯)) 0
have hf : ∀ (x : (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀)) : Type w)),
  Eq (α := (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₁)) : Type w))
    ((AddCommGrpCat.Hom.hom
            (AddCommGrpCat.ofHom (postcomp hS.extClass X h) ≫ AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) :
          (a : (↑(AddCommGrpCat.of (Ext X S.X₃ n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext X S.X₂ n₁)) : Type w))
        x :
      (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₁)) : Type w))
    ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of (Ext X S.X₃ n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext X S.X₂ n₁)) : Type w))
        x :
      (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₁)) : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀)) (AddCommGrpCat.ofHom (postcomp hS.extClass X h))
      (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X ⋯)) ⋯).Exact
have this₁ : (ShortComplex.mk (X₁ :=
    Functor.obj (C := DerivedCategory C)
      (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
      (Triangle.obj₃ hS.singleTriangle))
    (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
      hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) sorry)
    (Functor.map
      (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₁ : ℤ))
      (Triangle.mor₁ hS.singleTriangle))
    sorry).Exact
Tactic: have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₁ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk (X₁ :=
      Functor.obj (C := DerivedCategory C)
        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₃ hS.singleTriangle))
      (Functor.homologySequenceδ (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X)))
        hS.singleTriangle (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯)
      (Functor.map
        (Functor.shift (Functor.obj preadditiveCoyoneda (op (Functor.obj (singleFunctor C 0) X))) (M := ℤ) (↑n₁ : ℤ))
        (Triangle.mor₁ hS.singleTriangle))
      ⋯).Exact
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀)) (AddCommGrpCat.ofHom (postcomp hS.extClass X h))
      (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X ⋯)) ⋯).Exact
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₁ : ℕ
x₁ : Ext.{w, v, u} X S.X₁ n₁
hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
⊢ ∃ (x₃ : Ext.{w, v, u} X S.X₃ n₀), x₃.comp hS.extClass hn₀ = x₁
have this : (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀)) (AddCommGrpCat.ofHom (postcomp hS.extClass X hn₀))
    (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) sorry).Exact
Tactic: have := covariant_sequence_exact₁' X hS n₀ n₁ hn₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
x₂ : Ext.{w, v, u} X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
⊢ ∃ (x₁ : Ext.{w, v, u} X S.X₁ n), x₁.comp (mk₀ S.f) ⋯ = x₂
have this : (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry))
    (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).Exact
Tactic: have := covariant_sequence_exact₂' X hS n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext.{w, v, u} X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
⊢ ∃ (x₂ : Ext.{w, v, u} X S.X₂ n₀), x₂.comp (mk₀ S.g) ⋯ = x₃
have this : (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry))
    (AddCommGrpCat.ofHom (postcomp hS.extClass X hn₁)) sorry).Exact
Tactic: have := covariant_sequence_exact₃' X hS n₀ n₁ hn₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ Function.Injective.{w + 1, w + 1} (α := Ext.{w, v, u} L M 0) (β := Ext.{w, v, u} L N 0)
    (⇑(postcomp (mk₀ f) L ⋯) : (a : Ext L M 0) → Ext L N 0)
have rw : ∀ (x : Ext.{w, v, u} L M 0),
  Membership.mem (γ := AddSubgroup (Ext.{w, v, u} L M 0)) (AddMonoidHom.ker (postcomp (mk₀ f) L sorry)) x → x = 0
Tactic: rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]