awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x (a + x) ⋯ b).hom ≫
      K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv
have dsimp : CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h)
    ((Functor.obj (shiftFunctor₁ C x) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
      K.ιTotal (up ℤ) (p + x) q (n + x) sorry) =
  𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) sorry ≫ 𝟙 ((K.total (up ℤ)).X (n + x))
Tactic: dsimp [totalShift₁Iso, totalShift₁XIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' n' : ℤ
ha' : a' + b = n'
hn' : n' = n + x
⊢ K.ιTotal (up ℤ) a' b n' ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h
have subst : ∀ (ha' : a' + b = n + x),
  K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) sorry).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' sorry b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h
Tactic: subst hn'
Cleared hypotheses: n', ha', hn'
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' + b = n + x
⊢ K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) a b n h
have obtain : ∀ (h : a' - x + b = n),
  K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) sorry).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso (a' - x) x a' sorry b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h
Tactic: obtain rfl : a = a' - x := by lia
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x : ℤ
inst_2 : K.HasTotal (up ℤ)
b n a' : ℤ
ha' : a' + b = n + x
h : a' - x + b = n
⊢ K.ιTotal (up ℤ) a' b (n + x) ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₁Iso x)) n =
    (K.shiftFunctor₁XXIso (a' - x) x a' ⋯ b).inv ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h
have dsimp : Eq (α := (K.X a').X b ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
  (K.ιTotal (up ℤ) a' b (n + x) ha' ≫
    𝟙 ((K.total (up ℤ)).X (n + x)) ≫
      K.totalDesc fun (p q : ℤ) (hpq : p + q = n + x) ↦
        eqToHom sorry ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (p - x) q n sorry)
  (eqToHom sorry ≫ (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) (a' - x) b n h)
Tactic: dsimp [totalShift₁Iso, totalShift₁XIso, shiftFunctor₁XXIso, XXIsoOfEq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
⊢ Eq (α :=
    (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
      Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))
    (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x) :
      (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))
    (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
        (Iso.hom (K.totalShift₁Iso x))
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (total.map f (up ℤ))) :
      (Functor.obj (shiftFunctor₁ C x) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ)))
have h : ∀ (n i₁ i₂ : ℤ) (h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n),
  Eq (α :=
    ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n)
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₁Iso x))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n))
Tactic: ext n i₁ i₂ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ Eq (α :=
    ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n)
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ) ≫ Iso.hom (L.totalShift₁Iso x)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₁Iso x))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) x) (L.total (up ℤ))).X n))
have h₁ : Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
  (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
    (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ)) n ≫
      HomologicalComplex.Hom.f (Iso.hom (L.totalShift₁Iso x)) n))
  (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h :
      ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n)
        (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)) :
      ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + x)))
Tactic: dsimp at h ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₁Iso x)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₁ C x) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)) :
        ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + x)))
have h₁ : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) i₁) i₂ ≫
    (L.shiftFunctor₁XXIso i₁ x (i₁ + x) sorry i₂).hom ≫
      L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫ (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) sorry).inv =
  (K.shiftFunctor₁XXIso i₁ x (i₁ + x) sorry i₂).hom ≫
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) sorry).inv ≫
        HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
Tactic: rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
    K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (shiftFunctor₁ C x) f) i₁) i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₁ : HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
    𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
  𝟙 ((K.X (i₁ + x)).X i₂) ≫
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₁ : HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
  𝟙 ((K.X (i₁ + x)).X i₂) ≫
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
Tactic: rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₂ : HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
  K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫
    𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
Tactic: rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₂ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₃ : HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
  CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry)
    (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x))
Tactic: rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₂ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₃ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x))
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₄ : Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
  (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry)
  (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry)
    (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)))
Tactic: rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₂ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
      𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
h₃ :
  HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x))
h₄ :
  Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
    (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + x)) (K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)))
⊢ HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        𝟙 ((K.total (up ℤ)).X (n + x)) ≫ HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + x)
have h₅ : Eq (α := (K.X (i₁ + x)).X i₂ ⟶ (L.total (up ℤ)).X (n + x))
  (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry)
  (HomologicalComplex.Hom.f (f.f (i₁ + x)) i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) sorry)
Tactic: rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h : n + y = n'
⊢ CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
      ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow (K.ιTotal (up ℤ) p (q + y) n' ⋯))
      (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
        HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
          (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
            (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n ⋯)) =
    𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
have h₁ : ∀ (p q : ℤ) (h_1 : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n),
  CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h_1)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
        ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n' sorry))
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
            (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫
              (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n sorry))) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h_1 ≫
      𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
Tactic: ext p q h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n' : ℤ
h_1 : n + y = n'
p q : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n
⊢ CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
        ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n) ↦
          HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow
            (K.ιTotal (up ℤ) p (q + y) n' ⋯))
        (K.totalDesc fun (p q : ℤ) (hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n') ↦
          HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
            (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯) ≫
              (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n ⋯))) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h ≫
      𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
have h₁ : CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h)
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X n')
      ((Functor.obj (shiftFunctor₂ C y) K).totalDesc fun (p q : ℤ) (hpq : p + q = n) ↦
        HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n') (p * y).negOnePow (K.ιTotal (up ℤ) p (q + y) n' sorry))
      (K.totalDesc fun (p q : ℤ) (hpq : p + q = n') ↦
        HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
          (Iso.inv (XXIsoOfEq C (up ℤ) (up ℤ) K sorry sorry) ≫
            (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n sorry))) =
  (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n h ≫ 𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
Tactic: dsimp