awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ Eq (α :=
    Functor.obj (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁))
      (Opposite.op A))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryTheory.Functor.map yoneda
            (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
              NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (triangle S.f).obj₃ ≫
                Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
                  NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) (triangle S.f).obj₁ ≫
                    NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁))
          (Opposite.op A)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryTheory.Functor.map yoneda
            (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
              hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
          (Opposite.op A)))
      x)
have a : x ≫
    CategoryStruct.comp (Y :=
      Functor.obj (homologyFunctor C (up ℤ) n₀) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
      (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f))
      (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
        CategoryStruct.comp (Y := Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
          (Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry :
            Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₀) (mappingCone S.f) ⟶
              Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
          (CategoryStruct.comp (Y :=
              Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (Functor.obj (quotient C (up ℤ)) S.X₁))
              (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
              (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁) :
            Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁ ⟶
              HomologicalComplex.homology S.X₁ n₁)) =
  x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 (S.X₁.homology n₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫
      CategoryStruct.comp (Y :=
        Functor.obj (homologyFunctor C (up ℤ) n₀) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f))
        (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
          CategoryStruct.comp (Y := Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
            (Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ :
              Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₀) (mappingCone S.f) ⟶
                Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁)
            (CategoryStruct.comp (Y :=
                Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (Functor.obj (quotient C (up ℤ)) S.X₁))
                (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
                (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁) :
              Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁ ⟶
                HomologicalComplex.homology S.X₁ n₁)) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ 𝟙 (S.X₁.homology n₁)
have a : x ≫
    Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry ≫
      𝟙 (HomologicalComplex.homology S.X₁ n₁) =
  x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
Tactic: simp only [Iso.inv_hom_id_app, HomologicalComplex.homologyFunctor_obj, Iso.inv_hom_id_app_assoc,
    comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ ≫
        𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
have a : x ≫ Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry =
  x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
Tactic: erw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ x ≫ Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯ =
    x ≫ HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h
have a : CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
    (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ sorry w)
    (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry) =
  HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ sorry sorry ≫
    HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Tactic: rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
    HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
have a : ∀ (a : A' ⟶ S.X₁.X n₁) (b : A' ⟶ S.X₂.X n₀)
  (hab :
    x' =
      HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ sorry)
        (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)),
  CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ sorry w)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ sorry sorry ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Tactic: obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
have w₁ : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
Tactic: rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
    assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
    d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
    add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
    d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
| HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
    HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
have simp : HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ sorry sorry ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Tactic: simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
    inl_v_descShortComplex_f, comp_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
have a₁ : CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
    (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ sorry w_2)
    (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry) =
  HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ sorry sorry ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Tactic: conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
    inl_v_descShortComplex_f, comp_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯) =
    HomologicalComplex.liftCycles S.X₃ (b ≫ S.g.f n₀) n₁ ⋯ ⋯ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
have a₁ : Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
  (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
    (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ sorry w_2)
    (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ sorry))
  (S.X₁.liftCycles (-a) (n₁ + 1) sorry sorry ≫ S.X₁.homologyπ n₁)
Tactic: rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
    (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        Functor.shiftMap (HomologicalComplex.homologyFunctor C (up ℤ) 0) (triangle S.f).mor₃ n₀ n₁ ⋯))
    (S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁)
have a₁ : Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
  (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
    (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ sorry w_2)
    (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
      CategoryStruct.comp (Y :=
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 1) S.X₁).homology
          n₀)
        (HomologicalComplex.homologyMap (triangle S.f).mor₃ n₀)
        (NatTrans.app (Iso.hom (Functor.shiftIso (HomologicalComplex.homologyFunctor C (up ℤ) 0) 1 n₀ n₁ sorry)) S.X₁)))
  (S.X₁.liftCycles (-a) (n₁ + 1) sorry sorry ≫ S.X₁.homologyπ n₁)
Tactic: dsimp [Functor.shiftMap, homologyFunctor_shift]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ Eq (α := A' ⟶ HomologicalComplex.homology S.X₁ n₁)
    (CategoryStruct.comp (Y := HomologicalComplex.cycles (mappingCone S.f) n₀)
      (HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2)
      (HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 1)
                S.X₁).homology
            n₀)
          (HomologicalComplex.homologyMap (triangle S.f).mor₃ n₀)
          (NatTrans.app (Iso.hom (Functor.shiftIso (HomologicalComplex.homologyFunctor C (up ℤ) 0) 1 n₀ n₁ ⋯)) S.X₁)))
    (S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁)
have a₁ : HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ sorry).hom) (n₁ + 1)
      sorry sorry ≫
    HomologicalComplex.homologyπ S.X₁ n₁ ≫
      𝟙 (Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁) =
  S.X₁.liftCycles (-a) (n₁ + 1) sorry sorry ≫ S.X₁.homologyπ n₁
Tactic: rw [HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
    S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by lia) (n₁ + 1) (by simp),
    Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)
A' : C
π : A' ⟶ A
w_1 : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w_2 : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w_2 ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : Eq (α := A' ⟶ S.X₁.X (n₁ + 1)) (a ≫ S.X₁.d n₁ (n₁ + 1)) 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab :
  x' =
    HAdd.hAdd (α := A' ⟶ (mappingCone S.f).X n₀) (a ≫ HomComplex.Cochain.v (inl S.f) n₁ n₀ ⋯)
      (b ≫ HomologicalComplex.Hom.f (inr S.f) n₀)
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫
        𝟙 (Functor.obj (Functor.shift (HomologicalComplex.homologyFunctor C (up ℤ) 0) n₁) S.X₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
have a₁ : HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ sorry).hom) (n₁ + 1)
      sorry sorry ≫
    HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) =
  S.X₁.liftCycles (-a) (n₁ + 1) sorry sorry ≫ S.X₁.homologyπ n₁
Tactic: dsimp [homologyFunctor_shift]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
⊢ QuasiIsoAt (descShortComplex S) n
have rw : IsIso (X := HomologicalComplex.homology (mappingCone S.f) n) (Y := HomologicalComplex.homology S.X₃ n)
  (HomologicalComplex.homologyMap (descShortComplex S) n)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
⊢ (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast.map' 1 2
        _proof_246✝ _proof_363✝ ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n =
    NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝
have erw : Eq (α :=
  (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) sorry).δlast.obj
      (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 4 1)) ⟶
    (composableArrows₅ hS n (n + 1) sorry).δlast.obj' 2 _proof_363✝)
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
    CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor C (up ℤ) n) (triangle S.f).mor₂ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂ ≫
    (composableArrows₅ hS n (n + 1) sorry).δlast.map' 1 2 _proof_246✝ _proof_363✝)
Tactic: erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]