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 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
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₁ : (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • 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: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₂ : (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
  ((i₁ * y).negOnePow • 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: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₂ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₃ : (f.f i₁).f (i₂ + y) ≫
    HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) =
  ((i₁ * y).negOnePow • 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: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₂ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₃ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₄ : (f.f i₁).f (i₂ + y) ≫
    HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) =
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) ≫
    HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
Tactic: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₂ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₃ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₄ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₅ : HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
    ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) =
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) ≫
    HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
Tactic: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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
y : ℤ
inst_2 : K.HasTotal (up ℤ)
inst_3 : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
h₁ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₂ :
  (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₃ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    ((i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₄ :
  (f.f i₁).f (i₂ + y) ≫
      HSMul.hSMul (β := (L.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
h₅ :
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
      ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) =
    HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (K.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
        (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)
have h₆ : HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
    ((f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry) =
  HSMul.hSMul (β := (K.X i₁).X (i₂ + y) ⟶ (L.total (up ℤ)).X (n + y)) (i₁ * y).negOnePow
    (CategoryStruct.comp (Y := (K.total (up ℤ)).X (n + y)) (K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) sorry)
      (HomologicalComplex.Hom.f (total.map f (up ℤ)) (n + y)))
Tactic: rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
    Linear.units_smul_comp, ι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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
⊢ (Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
      Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y) =
    HSMul.hSMul (β :=
      (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
        Functor.obj
          (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙ shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
          (K.total (up ℤ)))
      (x * y).negOnePow
      (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
        (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
          Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
            Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))
have w : ∀ (n n₁ n₂ : ℤ) (h : (up ℤ).π (up ℤ) (up ℤ) (n₁, n₂) = n),
  (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f
        (Iso.hom
          ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
            Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y)))
        n =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      (HSMul.hSMul (β :=
              (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
                Functor.obj
                  (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙
                    shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
                  (K.total (up ℤ)))
              (x * y).negOnePow
              (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
                (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
                  Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
                    Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))).hom.f
        n
Tactic: ext n n₁ n₂ 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (n₁, n₂) = n
⊢ (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f
        (Iso.hom
          ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x ≪≫
            Functor.mapIso (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x) (K.totalShift₂Iso y)))
        n =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      (HSMul.hSMul (β :=
              (Functor.obj (shiftFunctor₂ C y ⋙ shiftFunctor₁ C x) K).total (up ℤ) ≅
                Functor.obj
                  (shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) y ⋙
                    shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) x)
                  (K.total (up ℤ)))
              (x * y).negOnePow
              (total.mapIso (Iso.app (shiftFunctor₁₂CommIso C x y) K) (up ℤ) ≪≫
                (Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y ≪≫
                  Functor.mapIso (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) y) (K.totalShift₁Iso x) ≪≫
                    Iso.app (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y) (K.total (up ℤ)))).hom.f
        n
have w : (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
    HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x)) n ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
  (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
    HSMul.hSMul (β :=
      ((Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).total (up ℤ)).X n ⟶
        (K.total (up ℤ)).X (n + x + y))
      (x * y).negOnePow
      (HomologicalComplex.Hom.f (total.map (NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K) (up ℤ)) n ≫
        HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y)) n ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
            HomologicalComplex.Hom.f
              (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n)
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 : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₂ C y) K).totalShift₁Iso x)) n ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      HSMul.hSMul (β :=
        ((Functor.obj (shiftFunctor₁ C x) (Functor.obj (shiftFunctor₂ C y) K)).total (up ℤ)).X n ⟶
          (K.total (up ℤ)).X (n + x + y))
        (x * y).negOnePow
        (HomologicalComplex.Hom.f (total.map (NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K) (up ℤ)) n ≫
          HomologicalComplex.Hom.f (Iso.hom ((Functor.obj (shiftFunctor₁ C x) K).totalShift₂Iso y)) n ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n)
have w : ((Functor.obj (shiftFunctor₂ C y) K).shiftFunctor₁XXIso n₁ x (n₁ + x) sorry n₂).hom ≫
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) sorry ≫
      (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)) x n (n + x) sorry).inv ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
  (x * y).negOnePow •
    (n₁ * y).negOnePow •
      ((NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K).f n₁).f n₂ ≫
        (((Functor.obj (shiftFunctor₁ C x) K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) sorry).hom ≫
            (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) sorry ≫
              (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)) y n (n + y)
                  sorry).inv) ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
            HomologicalComplex.Hom.f
              (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
Tactic: rw [Linear.comp_units_smul, ι_totalShift₁Iso_hom_f_assoc _ x n₁ n₂ n h _ rfl _ rfl,
    ιTotal_map_assoc, ι_totalShift₂Iso_hom_f_assoc _ y n₁ n₂ n h _ rfl _ rfl,
    Linear.units_smul_comp, Linear.comp_units_smul]
-- 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ ((Functor.obj (shiftFunctor₂ C y) K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        ((NatTrans.app (Iso.hom (shiftFunctor₁₂CommIso C x y)) K).f n₁).f n₂ ≫
          (((Functor.obj (shiftFunctor₁ C x) K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) ⋯).hom ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                (CochainComplex.shiftFunctorObjXIso ((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)) y n (n + y)
                    ⋯).inv) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
have w : 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
    (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) sorry ≫
      𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X (n + x)) ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
  (x * y).negOnePow •
    (n₁ * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
            (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) sorry ≫
              𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X (n + y))) ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
            HomologicalComplex.Hom.f
              (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
Tactic: dsimp [shiftFunctor₁₂CommIso]
-- 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ 𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
      (Functor.obj (shiftFunctor₂ C y) K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        𝟙 (((Functor.obj (shiftFunctor₂ C y) K).total (up ℤ)).X (n + x)) ≫
          HomologicalComplex.Hom.f (Iso.hom (K.totalShift₂Iso y)) (n + x) =
    (x * y).negOnePow •
      (n₁ * y).negOnePow •
        𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
          (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
              (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                𝟙 (((Functor.obj (shiftFunctor₁ C x) K).total (up ℤ)).X (n + y))) ≫
            HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
              HomologicalComplex.Hom.f
                (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
have w : (n₁ * y + x * y).negOnePow •
    Iso.hom (K.shiftFunctor₂XXIso (n₁ + x) n₂ y (n₂ + y) sorry) ≫
      K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry ≫
        Iso.inv (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y (n + x) (n + x + y) sorry) =
  (n₁ * y + x * y).negOnePow •
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) sorry ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
        HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
Tactic: rw [id_comp, id_comp, id_comp, id_comp, comp_id,
    ι_totalShift₂Iso_hom_f _ y (n₁ + x) n₂ (n + x) (by lia) _ rfl _ rfl, smul_smul,
    ← Int.negOnePow_add, add_mul, add_comm (x * y)]
-- 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 y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow •
      Iso.hom (K.shiftFunctor₂XXIso (n₁ + x) n₂ y (n₂ + y) ⋯) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          Iso.inv (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y (n + x) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
have w : (n₁ * y + x * y).negOnePow •
    𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
      K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) =
  (n₁ * y + x * y).negOnePow •
    (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) sorry ≫
      HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
        HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
Tactic: dsimp