awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Mono.{w, w + 1} (X := AddCommGrpCat.of (Ext.{w, v, u} L M 0)) (AddCommGrpCat.ofHom (postcomp (mk₀ f) L ⋯))

Tactic:
(AddCommGrpCat.mono_iff_injective _).mpr (postcomp_mk₀_injective_of_mono L f)

Premises used: Iff.mpr, AddCommGrpCat.mono_iff_injective, CategoryTheory.Abelian.Ext.postcomp_mk₀_injective_of_mono
-- 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
f : X ⟶ Y
n : ℕ
x : Ext.{w, v, u} Y Z n
⊢ 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)))
    (Functor.map (singleFunctor C 0) f ≫ x.hom) (comp (mk₀ f) x ⋯).hom

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

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.ShiftedHom.mk₀_comp, 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
Y_1 : C
inst_3 : HasDerivedCategory.{w', v, u} C
Y : C
n₀ : ℕ
x : Ext.{w, v, u} S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = 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
Y : C
n₀ : ℕ
x : Ext.{w, v, u} S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ Eq.{w' + 1} (α :=
    (↑(Functor.obj (C := (DerivedCategory.{w', v, u} C)ᵒᵖ)
          (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
          (Triangle.obj₁
            (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
              (op hS.singleTriangle)))) :
      Type w'))
    (Triangle.mor₃ hS.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) 1) x.hom ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) (↑n₀ : ℤ) 1 (↑n₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) Y))
    (hS.singleδ ≫
      Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑1 : ℤ)) x.hom ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) (↑n₀ : ℤ) (↑1 : ℤ) (↑n₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) Y))

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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
hf :
  ∀ (x : (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) : Type w)),
    Eq (α := (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n₁)) : Type w))
      ((AddCommGrpCat.Hom.hom
              (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯) ≫ AddCommGrpCat.ofHom (precomp hS.extClass Y h)) :
            (a : (↑(AddCommGrpCat.of (Ext S.X₂ Y n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext S.X₃ Y n₁)) : Type w))
          x :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n₁)) : Type w))
      ((AddCommGrpCat.Hom.hom 0 :
            (a : (↑(AddCommGrpCat.of (Ext S.X₂ Y n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext S.X₃ Y n₁)) : Type w))
          x :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n₁)) : Type w))
⊢ Eq.{w + 1} (α := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀) ⟶ AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n₁))
    (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯) ≫ AddCommGrpCat.ofHom (precomp hS.extClass Y h)) 0

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

Tactic:
simp only [ShortComplex.ShortExact.extClass_comp_assoc]

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc
-- 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
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (X₁ :=
      Functor.obj (C := (DerivedCategory C)ᵒᵖ)
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₂
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.map
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.mor₂
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
        (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle)) (↑n₀ : ℤ)
        (↑n₁ : ℤ) ⋯)
      ⋯).Exact

Tactic:
have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₃ _
    (op_distinguished _ 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk (X₁ :=
      Functor.obj (C := (DerivedCategory C)ᵒᵖ)
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₂
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.map
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.mor₂
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
        (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op 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} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯))
      (AddCommGrpCat.ofHom (precomp hS.extClass Y 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
hf :
  ∀ (x : (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₁ Y n₀)) : Type w)),
    Eq (α := (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₁)) : Type w))
      ((AddCommGrpCat.Hom.hom
              (AddCommGrpCat.ofHom (precomp hS.extClass Y h) ≫ AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) :
            (a : (↑(AddCommGrpCat.of (Ext S.X₁ Y n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext S.X₂ Y n₁)) : Type w))
          x :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₁)) : Type w))
      ((AddCommGrpCat.Hom.hom 0 :
            (a : (↑(AddCommGrpCat.of (Ext S.X₁ Y n₀)) : Type w)) → (↑(AddCommGrpCat.of (Ext S.X₂ Y n₁)) : Type w))
          x :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₁)) : Type w))
⊢ Eq.{w + 1} (α := AddCommGrpCat.of (Ext.{w, v, u} S.X₁ Y n₀) ⟶ AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₁))
    (AddCommGrpCat.ofHom (precomp hS.extClass Y h) ≫ AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) 0

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

Tactic:
simp only [ShortComplex.ShortExact.comp_extClass_assoc]

Premises used: CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc
-- 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
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (ShortComplex.mk (X₁ :=
      Functor.obj (C := (DerivedCategory C)ᵒᵖ)
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₃
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
        (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle)) (↑n₀ : ℤ)
        (↑n₁ : ℤ) ⋯)
      (Functor.map
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
        (Triangle.mor₁
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      ⋯).Exact

Tactic:
have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₁ _
    (op_distinguished _ 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  (ShortComplex.mk (X₁ :=
      Functor.obj (C := (DerivedCategory C)ᵒᵖ)
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
        (Triangle.obj₃
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
      (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
        (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle)) (↑n₀ : ℤ)
        (↑n₁ : ℤ) ⋯)
      (Functor.map
        (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
        (Triangle.mor₁
          (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op 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} S.X₁ Y n₀)) (AddCommGrpCat.ofHom (precomp hS.extClass Y h))
      (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) ⋯).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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ (contravariantSequence hS Y n₀ n₁ h).Exact

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

Premises used: CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁', CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂', CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃', 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext.{w, v, u} S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : comp hS.extClass x₁ hn₁ = 0
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯))
      (AddCommGrpCat.ofHom (precomp hS.extClass Y hn₁)) ⋯).Exact

Tactic:
have := contravariant_sequence_exact₁' hS Y 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext.{w, v, u} S.X₂ Y n
hx₂ : comp (mk₀ S.f) x₂ ⋯ = 0
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n)) (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯))
      (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).Exact

Tactic:
have := contravariant_sequence_exact₂' hS Y 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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext.{w, v, u} S.X₃ Y n₁
hx₃ : comp (mk₀ S.g) x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
⊢ (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₁ Y n₀)) (AddCommGrpCat.ofHom (precomp hS.extClass Y hn₀))
      (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) ⋯).Exact

Tactic:
have := contravariant_sequence_exact₃' hS Y 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
g : M ⟶ N
hg : Epi g
rw :
  ∀ (x : Ext.{w, v, u} N L 0),
    Membership.mem (γ := AddSubgroup (Ext.{w, v, u} N L 0)) (AddMonoidHom.ker (precomp (mk₀ g) L ⋯)) x → x = 0
⊢ Function.Injective.{w + 1, w + 1} (α := Ext.{w, v, u} N L 0) (β := Ext.{w, v, u} M L 0)
    (⇑(precomp (mk₀ g) L ⋯) : (a : Ext N L 0) → Ext M L 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
g : M ⟶ N
hg : Epi g
x : Ext.{w, v, u} N L 0
hx : Membership.mem (γ := AddSubgroup (Ext.{w, v, u} N L 0)) (AddMonoidHom.ker (precomp (mk₀ g) L ⋯)) x
obtain :
  ∀ (f : N ⟶ L)
    (hx :
      Membership.mem.{w, w} (α := Ext.{w, v, u} N L 0) (γ := AddSubgroup (Ext.{w, v, u} N L 0))
        (AddMonoidHom.ker (precomp (mk₀ g) L ⋯))
        ((AddEquiv.symm addEquiv₀ : (a : N ⟶ L) → Ext N L 0) f : Ext.{w, v, u} N L 0)),
    Eq.{w + 1} (α := Ext.{w, v, u} N L 0) ((AddEquiv.symm addEquiv₀ : (a : N ⟶ L) → Ext N L 0) f : Ext.{w, v, u} N L 0)
      (0 : Ext.{w, v, u} N L 0)
⊢ x = 0

Tactic:
obtain ⟨f, 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
g : M ⟶ N
hg : Epi g
f : N ⟶ L
hx :
  Membership.mem.{w, w} (α := Ext.{w, v, u} N L 0) (γ := AddSubgroup (Ext.{w, v, u} N L 0))
    (AddMonoidHom.ker (precomp (mk₀ g) L ⋯))
    ((AddEquiv.symm addEquiv₀ : (a : N ⟶ L) → Ext N L 0) f : Ext.{w, v, u} N L 0)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} N L 0) ((AddEquiv.symm addEquiv₀ : (a : N ⟶ L) → Ext N L 0) f : Ext.{w, v, u} N L 0)
    (0 : Ext.{w, v, u} N L 0)

Tactic:
simpa [← cancel_epi g] using hx

Premises used: CategoryTheory.cancel_epi
-- 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
g : M ⟶ N
hg : Epi g
⊢ Mono.{w, w + 1} (X := AddCommGrpCat.of (Ext.{w, v, u} N L 0)) (AddCommGrpCat.ofHom (precomp (mk₀ g) L ⋯))

Tactic:
(AddCommGrpCat.mono_iff_injective _).mpr (precomp_mk₀_injective_of_epi L g)

Premises used: Iff.mpr, CategoryTheory.Abelian.Ext.precomp_mk₀_injective_of_epi, AddCommGrpCat.mono_iff_injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
⊢ Eq.{w + 1} (α := Ext.{w, v, u} S.X₁ S.X₃ 0) (Ext.comp (Ext.mk₀ S.f) (Ext.mk₀ S.g) ⋯) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
dsimp :
  HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃) (Functor.obj (CochainComplex.singleFunctor C 0) S.X₁)
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (X₃ (S.map (CochainComplex.singleFunctor C 0))) (X₁ (S.map (CochainComplex.singleFunctor C 0)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃) (Functor.obj (CochainComplex.singleFunctor C 0) S.X₁)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
rw :
  HasSmallLocalizedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W
    (X₃ (S.map (CochainComplex.singleFunctor C 0))) (X₃ (S.map (CochainComplex.singleFunctor C 0)))
⊢ HasSmallLocalizedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W
    (X₃ (S.map (CochainComplex.singleFunctor C 0)))
    (CochainComplex.mappingCone (F := X₁ (S.map (CochainComplex.singleFunctor C 0)))
      (f (S.map (CochainComplex.singleFunctor C 0))))

Tactic:
rw [Localization.hasSmallLocalizedHom_iff_target W (S').X₃ qis hqis]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
⊢ HasSmallLocalizedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W
    (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃) (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃)

Tactic:
apply Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀ (M := ℤ)

Premises used: Int, CategoryTheory.Localization.hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
rw :
  HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (X₃ (S.map (CochainComplex.singleFunctor C 0))) (X₁ (S.map (CochainComplex.singleFunctor C 0)))
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (CochainComplex.mappingCone (F := X₁ (S.map (CochainComplex.singleFunctor C 0)))
      (f (S.map (CochainComplex.singleFunctor C 0))))
    (X₁ (S.map (CochainComplex.singleFunctor C 0)))

Tactic:
rw [Localization.hasSmallLocalizedShiftedHom_iff_source.{w} W ℤ qis hqis (S').X₁]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
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
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (X₃ (S.map (CochainComplex.singleFunctor C 0))) (X₁ (S.map (CochainComplex.singleFunctor C 0)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
Goal:
refine_3 : Eq (α := ℕ) sorry 0
refine_1 : Category.{?u.72276, ?u.72275} sorry
refine_2 : Abelian sorry
⊢ Eq (α := ℕ) sorry 0

Tactic:
letI := HasDerivedCategory.standard C
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
x : Ext.{w, v, u} X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (r • x).hom (x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯).hom
⊢ r • x = x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
x : Ext.{w, v, u} X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    (x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯).hom
⊢ HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((Equiv.linearEquiv R homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    (x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯).hom

Tactic:
change r • homEquiv x = (x.comp (mk₀ (r • 𝟙 Y)) (add_zero _)).hom

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Abelian.Ext.homEquiv, CategoryTheory.Abelian.Ext.hom, HSMul.hSMul, add_zero, DFunLike.coe, CategoryTheory.Abelian.Ext.mk₀