awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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, v} (X ⟶ Y)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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) ⋯
⊢ S.ShortExact

Tactic:
have hS : S.ShortExact :=
      { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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
x₃ : Ext S.X₃ Y (n + 1)
⊢ 1 + n = n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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
⊢ Function.Surjective (α := Ext S.X₁ Y n) (β := Ext S.X₃ Y (n + 1))
    (⇑(Ext.precomp hS.extClass Y ⋯) : (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)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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_2 : 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
this :
  Function.Surjective (α := Ext S.X₁ Y n) (β := Ext S.X₃ Y (n + 1))
    (⇑(Ext.precomp hS.extClass Y ⋯) : (a : Ext S.X₁ Y n) → Ext S.X₃ Y (n + 1))
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
small_of_surjective.{w} this

Premises used: small_of_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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_2 : 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
this :
  Function.Surjective (α := Ext S.X₁ Y n) (β := Ext S.X₃ Y (n + 1))
    (⇑(Ext.precomp hS.extClass Y ⋯) : (a : Ext S.X₁ Y n) → Ext S.X₃ Y (n + 1))
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
exact small_of_surjective.{w} this
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
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))
⊢ Small.{w, max u v} (Ext X Y n)

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

Premises used: small_congr, CategoryTheory.Abelian.Ext.homEquiv₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : HasDerivedCategory.{w', v, u} C
X Y Z : C
n : ℕ
x : Ext.{w, v, u} X Y n
f : Y ⟶ Z
⊢ Eq.{w' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Z)))
    (x.hom ≫
      Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑n : ℤ)) (Functor.map (singleFunctor C 0) f))
    (x.comp (mk₀ f) ⋯).hom

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.ShiftedHom.comp_mk₀, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X_1 : 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₁
⊢ HAdd.hAdd (α := ℤ) (↑n₀ : ℤ) 1 = (↑n₁ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
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₁ : ℤ) ⋯))
          (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₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) S.X₁))
⊢ 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₁ : ℤ))

Tactic:
rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.ShiftedHom.comp, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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.{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₁ : ℤ) ⋯))
          (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₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) S.X₁))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
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 ⋯) ≫ 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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
x : (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₂ n₀)) : Type w)
⊢ Eq (α := Ext.{w, v, u} X S.X₁ n₁) (comp (comp x (mk₀ S.g) ⋯) hS.extClass h) 0

Tactic:
simp only [comp_assoc_of_second_deg_zero, ShortComplex.ShortExact.comp_extClass,
          comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.ShortComplex.ShortExact.comp_extClass
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
⊢ HAdd.hAdd (α := ℤ) (↑n₀ : ℤ) 1 = (↑n₁ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁ :=
      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

Tactic:
have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₃ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (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

Tactic:
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢

Premises used: CategoryTheory.ShortComplex.ab_exact_iff_function_exact
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
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 ⋯)) :
            (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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
x : (↑(AddCommGrpCat.of (Ext.{w, v, u} X S.X₃ n₀)) : Type w)
⊢ Eq (α := Ext.{w, v, u} X S.X₂ n₁) (comp (comp x hS.extClass h) (mk₀ S.f) ⋯) 0

Tactic:
simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp,
          comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.ShortComplex.ShortExact.extClass_comp, CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁ :=
      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

Tactic:
have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₁ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (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

Tactic:
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢

Premises used: CategoryTheory.ShortComplex.ab_exact_iff_function_exact
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
⊢ (covariantSequence X hS n₀ n₁ h).Exact

Tactic:
exact_of_δ₀ (covariant_sequence_exact₂' X hS n₀).exact_toComposableArrows
    (exact_of_δ₀ (covariant_sequence_exact₃' X hS n₀ n₁ h).exact_toComposableArrows
      (exact_of_δ₀ (covariant_sequence_exact₁' X hS n₀ n₁ h).exact_toComposableArrows
        (covariant_sequence_exact₂' X hS n₁).exact_toComposableArrows))

Premises used: CategoryTheory.Abelian.Ext.covariant_sequence_exact₁', CategoryTheory.Abelian.Ext.covariant_sequence_exact₃', CategoryTheory.Abelian.Ext.covariant_sequence_exact₂', CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ComposableArrows.exact_of_δ₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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₁
⊢ (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 ⋯)) ⋯).Exact

Tactic:
have := covariant_sequence_exact₁' X hS n₀ n₁ hn₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X ⋯))
      (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯)) ⋯).Exact

Tactic:
have := covariant_sequence_exact₂' X hS n
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
⊢ (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 hn₁)) ⋯).Exact

Tactic:
have := covariant_sequence_exact₃' X hS n₀ n₁ hn₁
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
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 ⋯)) x → x = 0
⊢ 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)

Tactic:
rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]

Premises used: AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
x : Ext.{w, v, u} L M 0
hx : Membership.mem (γ := AddSubgroup (Ext.{w, v, u} L M 0)) (AddMonoidHom.ker (postcomp (mk₀ f) L ⋯)) x
obtain :
  ∀ (g : L ⟶ M)
    (hx :
      Membership.mem.{w, w} (α := Ext.{w, v, u} L M 0) (γ := AddSubgroup (Ext.{w, v, u} L M 0))
        (AddMonoidHom.ker (postcomp (mk₀ f) L ⋯))
        ((AddEquiv.symm addEquiv₀ : (a : L ⟶ M) → Ext L M 0) g : Ext.{w, v, u} L M 0)),
    Eq.{w + 1} (α := Ext.{w, v, u} L M 0) ((AddEquiv.symm addEquiv₀ : (a : L ⟶ M) → Ext L M 0) g : Ext.{w, v, u} L M 0)
      (0 : Ext.{w, v, u} L M 0)
⊢ x = 0

Tactic:
obtain ⟨g, rfl⟩ := Ext.addEquiv₀.symm.surjective x

Premises used: AddEquiv.surjective, CategoryTheory.Abelian.Ext.addEquiv₀, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
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
g : L ⟶ M
hx :
  Membership.mem.{w, w} (α := Ext.{w, v, u} L M 0) (γ := AddSubgroup (Ext.{w, v, u} L M 0))
    (AddMonoidHom.ker (postcomp (mk₀ f) L ⋯))
    ((AddEquiv.symm addEquiv₀ : (a : L ⟶ M) → Ext L M 0) g : Ext.{w, v, u} L M 0)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} L M 0) ((AddEquiv.symm addEquiv₀ : (a : L ⟶ M) → Ext L M 0) g : Ext.{w, v, u} L M 0)
    (0 : Ext.{w, v, u} L M 0)

Tactic:
simpa [← cancel_mono f] using hx

Premises used: CategoryTheory.cancel_mono