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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : 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₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
have pos : CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq)
    ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ 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)) =
  (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow
      (((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.D₂ (up ℤ) n₀' n₁')
Tactic: dsimp [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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : 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₀ hpq)
      ((Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ 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₁' ⋯)) =
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p q n₀ hpq ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
          GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
        y.negOnePow
        (((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₀' ⋯)) ≫
          K.D₂ (up ℤ) n₀' n₁')
have pos : (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q) •
    ((Functor.obj (shiftFunctor₂ C y) K).X p).d q (q + 1) ≫
      HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
        (K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry) =
  HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁')
    (y.negOnePow * (p * y).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q + y))
    ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry)
Tactic: rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, Linear.units_smul_comp,
      smul_smul, ι_D₂, ((shiftFunctor₂ C y).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ (show q + y + 1 = q + 1 + y by lia) _ (by dsimp; lia),
      Linear.units_smul_comp, Category.assoc, smul_smul, ι_totalDesc]
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q) •
      ((Functor.obj (shiftFunctor₂ C y) K).X p).d q (q + 1) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁')
      (y.negOnePow * (p * y).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q + y))
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
have pos : p.negOnePow •
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.X p).X (q + 1 + y)) y.negOnePow ((K.X p).d (q + y) (q + 1 + y)) ≫
      HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
        (K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry) =
  HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y.negOnePow * (p * y).negOnePow * p.negOnePow)
    ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry)
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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p.negOnePow •
      HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.X p).X (q + 1 + y)) y.negOnePow ((K.X p).d (q + y) (q + 1 + y)) ≫
        HSMul.hSMul (β := (K.X p).X (q + 1 + y) ⟶ (K.total (up ℤ)).X n₁') (p * y).negOnePow
          (K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y.negOnePow * (p * y).negOnePow * p.negOnePow)
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
have pos : HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p + y + p * y).negOnePow
    ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry) =
  HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y + p).negOnePow
    ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' sorry)
Tactic: rw [Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, smul_smul,
      ← Int.negOnePow_add, ← Int.negOnePow_add, ← Int.negOnePow_add,
      ← Int.negOnePow_add]
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (p + y + p * y).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    HSMul.hSMul (β := (K.X p).X (q + y) ⟶ (K.total (up ℤ)).X n₁') (y + p * y + p).negOnePow
      ((K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯)
have pos : p + y + p * y = y + p * y + p
Tactic: congr 2
-- 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ (Functor.obj (shiftFunctor₂ C y) K).D₂ (up ℤ) n₀ n₁ ≫ Iso.hom (K.totalShift₂XIso y n₁ n₁' h₁) =
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n₀ ⟶
        GradedObject.mapObj.{0, 0, v_1, u_1} K.toGradedObject ((up ℤ).π (up ℤ) (up ℤ)) n₁')
      y.negOnePow (Iso.hom (K.totalShift₂XIso y n₀ n₀' h₀) ≫ K.D₂ (up ℤ) n₀' n₁')
have neg : ¬(up ℤ).Rel n₀' n₁'
Tactic: rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (hypothesis)
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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'
have h₂ : ¬n₀ + 1 = n₁
Tactic: simp_all only [up_Rel]
Cleared hypotheses: 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 : (up ℤ).Rel n n'
⊢ Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₂XIso y n (n + y) ⋯ :
              ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + y)))
          n) ≫
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ))).d n n' =
    ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).d n n' ≫
      Iso.hom
        ((fun (n : ℤ) ↦
            (K.totalShift₂XIso y n (n + y) ⋯ :
              ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X (n + y)))
          n')
have dsimp : Iso.hom (K.totalShift₂XIso y n (n + y) sorry) ≫
    HSMul.hSMul (β := (K.total (up ℤ)).X (n + y) ⟶ (K.total (up ℤ)).X (n' + y)) y.negOnePow
      ((K.total (up ℤ)).d (n + y) (n' + y)) =
  ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).d n n' ≫ Iso.hom (K.totalShift₂XIso y n' (n' + y) sorry)
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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv
have subst : (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫ HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
  (a * y).negOnePow •
    (K.shiftFunctor₂XXIso a b y (b + y) sorry).hom ≫
      K.ιTotal (up ℤ) a (b + y) (n + y) sorry ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) sorry).inv
Tactic: subst hb' hn'
Cleared hypotheses: b', hb', n', 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv
have dsimp : CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
    ((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 + y)) (p * y).negOnePow
        (K.ιTotal (up ℤ) p (q + y) (n + y) sorry)) =
  (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) sorry ≫ 𝟙 ((K.total (up ℤ)).X (n + y))
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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ K.ιTotal (up ℤ) a b' n' hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
have subst : ∀ (hb' : a + b' = n + y),
  K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) sorry).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a b y b' sorry).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
Tactic: subst hn'
Cleared hypotheses: n', hb', 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : a + b' = n + y
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a b n h)
have obtain : ∀ (h : a + (b' - y) = n),
  K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) sorry).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a (b' - y) y b' sorry).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a (b' - y) n h)
Tactic: obtain rfl : b = b' - y := by lia
Cleared hypotheses: b, 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 ℤ)
y : ℤ
inst_2 : K.HasTotal (up ℤ)
a n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫
        HomologicalComplex.Hom.f (Iso.inv (K.totalShift₂Iso y)) n =
    HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
      ((K.shiftFunctor₂XXIso a (b' - y) y b' ⋯).inv ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a (b' - y) n h)
have dsimp : (K.ιTotal (up ℤ) a b' (n + y) hb' ≫
    𝟙 ((K.total (up ℤ)).X (n + y)) ≫
      K.totalDesc fun (p q : ℤ) (hpq : p + q = n + y) ↦
        HSMul.hSMul (β := (K.X p).X q ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (p * y).negOnePow
          (eqToHom sorry ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) p (q - y) n sorry)) =
  HSMul.hSMul (β := (K.X a).X b' ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n) (a * y).negOnePow
    (eqToHom sorry ≫ (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) a (b' - y) 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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
⊢ Eq (α :=
    (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
      Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ)))
    (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y) :
      (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ)))
    (CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
        (Iso.hom (K.totalShift₂Iso y))
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (total.map f (up ℤ))) :
      (Functor.obj (shiftFunctor₂ C y) K).total (up ℤ) ⟶
        Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ)))
have h : ∀ (n i₁ i₂ : ℤ) (h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n),
  Eq (α :=
    ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ))).X n)
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₂Iso y))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (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
y : ℤ
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 y) K).X i₁).X i₂ ⟶
      (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ))).X n)
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f
        (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ) ≫ Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.total (up ℤ)))
            (Iso.hom (K.totalShift₂Iso y))
            (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y)
              (total.map f (up ℤ))))
          n :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶
          (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (L.total (up ℤ))).X n))
have h₁ : Eq (α := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y))
  (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
    (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ)) n ≫
      HomologicalComplex.Hom.f (Iso.hom (L.totalShift₂Iso y)) n))
  (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
    ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
      ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n)
        (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)) :
      ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + y)))
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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ Eq (α := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h)
      (HomologicalComplex.Hom.f (total.map (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (L.totalShift₂Iso y)) n))
    (CategoryStruct.comp (Y := ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      ((Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) i₁ i₂ n h :
        ((Functor.obj (shiftFunctor₂ C y) K).X i₁).X i₂ ⟶ ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n)
      (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) n)
          (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)) :
        ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X n ⟶ (L.total (up ℤ)).X (n + y)))
have h₁ : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (shiftFunctor₂ C y) f) i₁) i₂ ≫
    ((i₁ * y).negOnePow •
      (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) sorry).hom ≫
        L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) sorry).inv) =
  ((i₁ * y).negOnePow •
      (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) sorry).hom ≫
        K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) sorry).inv) ≫
    HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
Tactic: rw [ιTotal_map_assoc, L.ι_totalShift₂Iso_hom_f y i₁ i₂ n h _ rfl _ rfl,
    K.ι_totalShift₂Iso_hom_f_assoc y 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
y : ℤ
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 y) f) i₁) i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((i₁ * y).negOnePow •
        (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₁ : (f.f i₁).f (i₂ + y) ≫
    ((i₁ * y).negOnePow •
      𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
  ((i₁ * y).negOnePow •
      𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
    HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
Tactic: dsimp