awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ x = 0
have 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 sorry))
      ((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: obtain ⟨g, rfl⟩ := Ext.addEquiv₀.symm.surjective x
Cleared hypotheses: x, hx
-- 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
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ 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
have 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 sorry) ≫ 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))
Tactic: ext
-- 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
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₁ := 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
have 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₁ : ℤ) sorry)
    sorry).Exact
Tactic: have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₃ _
    (op_distinguished _ 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
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
⊢ (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
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
S : ShortComplex.{v, u} C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ 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
have 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 sorry)) :
          (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))
Tactic: ext
-- 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
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₁ := 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
have 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₁ : ℤ) sorry)
    (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))))
    sorry).Exact
Tactic: have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₁ _
    (op_distinguished _ 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
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
⊢ (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
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
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
⊢ ∃ (x₂ : Ext.{w, v, u} S.X₂ Y n₀), comp (mk₀ S.f) x₂ ⋯ = x₁
have this : (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y sorry))
    (AddCommGrpCat.ofHom (precomp hS.extClass Y hn₁)) sorry).Exact
Tactic: have := contravariant_sequence_exact₁' hS Y 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
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
⊢ ∃ (x₁ : Ext.{w, v, u} S.X₃ Y n), comp (mk₀ S.g) x₁ ⋯ = x₂
have this : (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n)) (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y sorry))
    (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y sorry)) sorry).Exact
Tactic: have := contravariant_sequence_exact₂' hS Y 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
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₁
⊢ ∃ (x₁ : Ext.{w, v, u} S.X₁ Y n₀), comp hS.extClass x₁ hn₀ = x₃
have this : (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 sorry)) sorry).Exact
Tactic: have := contravariant_sequence_exact₃' hS Y 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
g : M ⟶ N
hg : Epi g
⊢ 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)
have 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 sorry)) x → x = 0
Tactic: rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]
-- 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
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
⊢ x = 0
have 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 sorry))
      ((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: obtain ⟨f, rfl⟩ := Ext.addEquiv₀.symm.surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass (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
⊢ HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) W ℤ
    (X₃ (S.map (CochainComplex.singleFunctor C 0))) (X₁ (S.map (CochainComplex.singleFunctor C 0)))
have 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₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass (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
⊢ 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))))
have 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)))
Tactic: rw [Localization.hasSmallLocalizedHom_iff_target W (S').X₃ qis hqis]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass (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
⊢ 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)))
have 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)))
Tactic: rw [Localization.hasSmallLocalizedShiftedHom_iff_source.{w} W ℤ qis hqis (S').X₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass (goal)
Goal:
refine_3 : Eq (α := ℕ) sorry 0
⊢ Eq (α := ℕ) sorry 0
have refine_1 : Category.{?u.72276, ?u.72275} sorry
Tactic: letI := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass (goal)
Goal:
refine_3 : Eq (α := ℕ) sorry 0
refine_1 : Category.{?u.72276, ?u.72275} sorry
⊢ Eq (α := ℕ) sorry 0
have refine_2 : Abelian sorry
Tactic: letI := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (goal)
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
⊢ r • x = x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯
have 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))) sorry).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (goal)
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
⊢ 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
have 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))) sorry).hom
Tactic: change r • homEquiv x = (x.comp (mk₀ (r • 𝟙 Y)) (add_zero _)).hom
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (goal)
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
⊢ 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
have 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 : ℤ)) =
  ShiftedHom.comp x.hom (hom (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y)))) sorry
Tactic: rw [comp_hom, mk₀_hom, Functor.map_smul, Functor.map_id, ShiftedHom.mk₀_smul,
    ShiftedHom.comp_smul, ShiftedHom.comp_mk₀_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (goal)
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 : ℤ)) =
    ShiftedHom.comp x.hom (hom (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y)))) ⋯
⊢ 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
have 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 : ℤ)) =
  ShiftedHom.comp x.hom
    (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1
      (Functor.map (DerivedCategory.singleFunctor C 0) (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))))
    sorry
Tactic: rw [comp_hom, mk₀_hom, Functor.map_smul, Functor.map_id, ShiftedHom.mk₀_smul,
    ShiftedHom.comp_smul, ShiftedHom.comp_mk₀_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj Q S.X₃))
      (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
        (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁))))
    (Functor.map F.mapDerivedCategory (triangleOfSESδ hS))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) S.X₃ ≫
      CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj Q (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) S.X₁)))
        (triangleOfSESδ ⋯)
        (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
            (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors) S.X₁) ≫
          NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1)) (Functor.obj Q S.X₁)))
have this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
Tactic: have := CochainComplex.mappingCone.quasiIso_descShortComplex hS