awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
⊢ Eq (α := MorphismProperty (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)))
    (MorphismProperty.inverseImage (quasiIso C (up ℤ))
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n))
    (quasiIso C (up ℤ))
have h : ∀ ⦃X Y : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)⦄ (f : X ⟶ Y),
  MorphismProperty.inverseImage (quasiIso C (up ℤ))
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) f ↔
    quasiIso C (up ℤ) f
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0
have hj₁ : i + 1 = j
Tactic: simp only [next] at hj hj'
Cleared hypotheses: hj, hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
hj₁ : i + 1 = j
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0
have hj'₁ : i' + 1 = j'
Tactic: simp only [next] at hj hj'
Cleared hypotheses: hj, hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0
have obtain : ∀ (hi' : n + i = i + n) (hj' : i + n + 1 = j'), (f ≫ (K.shiftFunctorObjXIso n i (i + n) sorry).hom) ≫ K.d (i + n) j' = 0
Tactic: obtain rfl : i' = i + n := by lia
Cleared hypotheses: i', hi', hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0
have obtain : ∀ (hj' : i + n + 1 = j + n),
  Eq (α := A ⟶ K.X (j + n)) ((f ≫ (K.shiftFunctorObjXIso n i (i + n) sorry).hom) ≫ K.d (i + n) (j + n)) 0
Tactic: obtain rfl : j' = j + n := by lia
Cleared hypotheses: j', hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ Eq (α := A ⟶ K.X (j + n)) ((f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) (j + n)) 0
have dsimp : Eq (α := A ⟶ K.X (j + n)) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) 0
Tactic: dsimp at hf ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ HSMul.hSMul (β := K.X (i + n) ⟶ K.X (j + n)) n.negOnePow (K.d (i + n) (j + n)) = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ Eq (α := A ⟶ K.X (j + n)) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) 0
have hf₁ : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
Tactic: simp only [Linear.comp_units_smul] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
⊢ Eq (α := A ⟶ K.X (j + n)) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) 0
have apply : HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
Tactic: apply (one_smul (M := ℤˣ) _).symm.trans _
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
⊢ HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
have rw : HSMul.hSMul (β := A ⟶ K.X (j + n)) (n.negOnePow * n.negOnePow) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
Tactic: rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
rw : HSMul.hSMul (β := A ⟶ K.X (j + n)) (n.negOnePow * n.negOnePow) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
⊢ HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
have rw₁ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
Tactic: rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
rw : HSMul.hSMul (β := A ⟶ K.X (j + n)) (n.negOnePow * n.negOnePow) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
rw₁ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
⊢ HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
have rw₂ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
Tactic: rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
rw : HSMul.hSMul (β := A ⟶ K.X (j + n)) (n.negOnePow * n.negOnePow) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
rw₁ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
rw₂ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
⊢ HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
have rw₃ : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow 0 = 0
Tactic: rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
rw : HSMul.hSMul (β := A ⟶ K.X (j + n)) (n.negOnePow * n.negOnePow) ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
rw₁ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
rw₂ : n.negOnePow • HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow (f ≫ K.d (i + n) (j + n)) = 0
rw₃ : HSMul.hSMul (β := A ⟶ K.X (j + n)) n.negOnePow 0 = 0
⊢ HSMul.hSMul (α := ℤˣ) (β := A ⟶ K.X (j + n)) 1 ((f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n)) = 0
have rw₄ : Eq.{v_1 + 1} (α := A ⟶ K.X (j + n)) 0 0
Tactic: rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ Eq (α := A ⟶ homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) i)
    (liftCycles (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) f j hj hf ≫
      homologyπ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) i)
    (CategoryStruct.comp (Y := cycles K i') (liftCycles K (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯)
      (homologyπ K i' ≫ NatTrans.app (Iso.inv (Functor.shiftIso (homologyFunctor C (up ℤ) 0) n i i' hi')) K))
have simp : Eq (α := A ⟶ homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) i)
  ((sc (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) i).liftCycles f sorry ≫
    (sc (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) i).homologyπ)
  ((Functor.obj (shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i) K).liftCycles f sorry ≫
    (Functor.obj (shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i) K).homologyπ)
Tactic: simp only [liftCycles, homologyπ,
    shiftFunctorObjXIso, Functor.shiftIso, Functor.ShiftSequence.shiftIso,
    ShiftSequence.shiftIso_inv_app, ShortComplex.homologyπ_naturality,
    ShortComplex.liftCycles_comp_cyclesMap_assoc, shiftShortComplexFunctorIso_inv_app_τ₂,
    assoc, Iso.hom_inv_id, 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₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃
have h : ∀ (i : ℤ),
  HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ descShortComplex S₂) i = (descShortComplex S₁ ≫ f.τ₃).f i
Tactic: ext i
-- 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₁
⊢ Eq (α :=
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₀) (triangleh S.f).obj₃ ⟶
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (triangleh S.f).obj₁)
    (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n₀ n₁ h)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
have dsimp : Eq (α :=
  Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₀) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)) ⟶
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁) (Functor.obj (quotient C (up ℤ)) S.X₁))
  (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
      (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
        (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
      n₀ n₁ h :
    Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₀)
        (Triangle.obj₃
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))) ⟶
      Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n₁)
        (Triangle.obj₁
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))))
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
    HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
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₁
⊢ Eq (α :=
    Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f) ⟶
      Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)
    (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
      Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n₀ n₁ h ≫
        NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁)
    (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁))
have a : Eq (α :=
  Quiver.Hom (V := CategoryTheory.Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
    (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)))
    (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
  (CategoryTheory.Functor.map yoneda
    (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
      Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n₀ n₁ h ≫
        NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁))
  (CategoryTheory.Functor.map yoneda
    (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
Tactic: apply yoneda.map_injective
-- 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₁
⊢ Eq (α :=
    Quiver.Hom (V := CategoryTheory.Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
      (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)))
      (Functor.obj yoneda (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
    (CategoryTheory.Functor.map yoneda
      (NatTrans.app (Iso.inv (homologyFunctorFactors C (up ℤ) n₀)) (mappingCone S.f) ≫
        Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
            (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
              (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
            n₀ n₁ h ≫
          NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n₁)) S.X₁))
    (CategoryTheory.Functor.map yoneda
      (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ 𝟙 (Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₁) S.X₁)))
have a : ∀ (A : C) (x : A ⟶ Functor.obj (HomologicalComplex.homologyFunctor C (up ℤ) n₀) (mappingCone S.f)),
  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) ≫
              Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
                  (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁)
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
                      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
                  n₀ n₁ h ≫
                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)
Tactic: ext ⟨A⟩ (x : A ⟶ _)
-- 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) ≫
              Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
                  (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁)
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
                    (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
                      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
                  n₀ n₁ h ≫
                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 : 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₁ sorry ≫
                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)
Tactic: erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]