awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
comm₄ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃
have comm₅ : T₁.mor₃ ≫
    CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
  (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫ T₂.mor₃
Tactic: simp only [ha', hb'] at comm₂ comm₃
Cleared hypotheses: comm₂, comm₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃
have refine_1 : T₁.mor₂ ≫ γ.hom₃ = b ≫ T₂.mor₂
Tactic: refine ⟨γ.hom₃, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
refine_1 : T₁.mor₂ ≫ γ.hom₃ = b ≫ T₂.mor₂
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃
have refine_2 : T₁.mor₃ ≫
    CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) a =
  γ.hom₃ ≫ T₂.mor₃
Tactic: refine ⟨γ.hom₃, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
⊢ HSMul.hSMul (β := K.X (i + n) ⟶ K.X (j + n)) n.negOnePow (K.d (i + n) (j + n)) = 0
have a : ¬(ComplexShape.up ℤ).Rel (i + n) (j + n)
Tactic: rw [K.shape, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel i j
hij' : (ComplexShape.up ℤ).Rel (i + n) (j + n)
⊢ False
have a : (ComplexShape.up ℤ).Rel i j
Tactic: apply hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
X Y : CochainComplex.{v, u, 0} C ℤ
φ : X ⟶ Y
i j : ℤ
h : (ComplexShape.up ℤ).Rel i j
⊢ φ.f (i + n) ≫
      { X := fun (i : ℤ) ↦ Y.X (i + n),
            d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := Y.X (x + n) ⟶ Y.X (x_1 + n)) n.negOnePow (Y.d (x + n) (x_1 + n)),
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }.d
        i j =
    { X := fun (i : ℤ) ↦ X.X (i + n),
            d := fun (x x_1 : ℤ) ↦ HSMul.hSMul (β := X.X (x + n) ⟶ X.X (x_1 + n)) n.negOnePow (X.d (x + n) (x_1 + n)),
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }.d
        i j ≫
      φ.f (j + n)
have dsimp : φ.f (i + n) ≫ HSMul.hSMul (β := Y.X (i + n) ⟶ Y.X (j + n)) n.negOnePow (Y.d (i + n) (j + n)) =
  HSMul.hSMul (β := X.X (i + n) ⟶ X.X (j + n)) n.negOnePow (X.d (i + n) (j + n)) ≫ φ.f (j + n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
h : n = 0
X Y : CochainComplex.{v, u, 0} C ℤ
x : X ⟶ Y
⊢ Eq (α := Functor.obj (shiftFunctor C n) X ⟶ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) Y)
    (CategoryTheory.Functor.map (shiftFunctor C n) x ≫
      Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
              Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
          Y))
    (Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i ⋯) ⋯ :
              Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (CochainComplex.{v, u, 0} C ℤ)) x)
have h₁ : ∀ (i : ℤ),
  Eq (α := (Functor.obj (shiftFunctor C n) X).X i ⟶ (Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) Y).X i)
    (Hom.f
      (CategoryTheory.Functor.map (shiftFunctor C n) x ≫
        Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i sorry) sorry :
                Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
            Y))
      i)
    (Hom.f
      (Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n i i sorry) sorry :
                Functor.obj (shiftFunctor C n) K ≅ Functor.obj (𝟭 (CochainComplex.{v, u, 0} C ℤ)) K))
            X) ≫
        CategoryTheory.Functor.map (𝟭 (CochainComplex.{v, u, 0} C ℤ)) x)
      i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h_1 : (ComplexShape.up ℤ).Rel x x_1
⊢ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) x) ≫
      (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
    (Functor.obj (shiftFunctor C n₁₂) K).d x x_1 ≫
      Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) x_1)
have subst : Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) sorry) x) ≫
    (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
  (Functor.obj (shiftFunctor C (n₁ + n₂)) K).d x x_1 ≫
    Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) sorry) x_1)
Tactic: subst h
Cleared hypotheses: n₁₂, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ : ℤ
K : CochainComplex.{v, u, 0} C ℤ
x x_1 : ℤ
h : (ComplexShape.up ℤ).Rel x x_1
⊢ Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x) ≫
      (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K).d x x_1 =
    (Functor.obj (shiftFunctor C (n₁ + n₂)) K).d x x_1 ≫
      Iso.hom ((fun (i : ℤ) ↦ K.shiftFunctorObjXIso (n₁ + n₂) i (i + n₂ + n₁) ⋯) x_1)
have dsimp : (XIsoOfEq K sorry).hom ≫
    (n₂.negOnePow •
      HSMul.hSMul (β := K.X (x + n₂ + n₁) ⟶ K.X (x_1 + n₂ + n₁)) n₁.negOnePow (K.d (x + n₂ + n₁) (x_1 + n₂ + n₁))) =
  HSMul.hSMul (β := K.X (x + (n₁ + n₂)) ⟶ K.X (x_1 + (n₁ + n₂))) (n₁ + n₂).negOnePow
      (K.d (x + (n₁ + n₂)) (x_1 + (n₁ + n₂))) ≫
    (XIsoOfEq K sorry).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
⊢ Eq (α := Functor.obj (shiftFunctor C n₁₂) X ⟶ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) Y)
    (CategoryTheory.Functor.map (shiftFunctor C n₁₂) f ≫
      Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
              Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
          Y))
    (Iso.hom
        ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯ :
              Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
          X) ≫
      CategoryTheory.Functor.map (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) f)
have h₁ : ∀ (i : ℤ),
  Eq (α := (Functor.obj (shiftFunctor C n₁₂) X).X i ⟶ (Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) Y).X i)
    (Hom.f
      (CategoryTheory.Functor.map (shiftFunctor C n₁₂) f ≫
        Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) sorry) sorry :
                Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
            Y))
      i)
    (Hom.f
      (Iso.hom
          ((fun (K : CochainComplex.{v, u, 0} C ℤ) ↦
              (Hom.isoOfComponents (fun (i : ℤ) ↦ K.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) sorry) sorry :
                Functor.obj (shiftFunctor C n₁₂) K ≅ Functor.obj (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) K))
            X) ≫
        CategoryTheory.Functor.map (shiftFunctor C n₁ ⋙ shiftFunctor C n₂) f)
      i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as = n + { as := a + b : Discrete ℤ }.as
have dsimp : n + b + a = n + (a + b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ n + b + a = n + (a + b)
have rw : n + b + a = n + (b + a)
Tactic: rw [add_comm a, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : n + b + a = n + (b + a)
⊢ n + b + a = n + (a + b)
have rw₁ : n + (b + a) = n + (b + a)
Tactic: rw [add_comm a, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ n + { as := a + b : Discrete ℤ }.as = n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as
have dsimp : n + (a + b) = n + b + a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ n + (a + b) = n + b + a
have rw : n + (b + a) = n + b + a
Tactic: rw [add_comm a, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : n + (b + a) = n + b + a
⊢ n + (a + b) = n + b + a
have rw₁ : n + (b + a) = n + (b + a)
Tactic: rw [add_comm a, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as = n + { as := ab : Discrete ℤ }.as
have dsimp : n + b + a = n + ab
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + b + a = n + ab
have rw : n + b + a = n + (a + b)
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + b + a = n + (a + b)
⊢ n + b + a = n + ab
have rw₁ : n + (b + a) = n + (a + b)
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + b + a = n + (a + b)
rw₁ : n + (b + a) = n + (a + b)
⊢ n + b + a = n + ab
have rw₂ : n + (b + a) = n + (b + a)
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b ab h)) K) n =
    (XIsoOfEq K ⋯).hom
have subst : Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) sorry)) K) n =
  (XIsoOfEq K sorry).hom
Tactic: subst h
Cleared hypotheses: ab, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
have rw : Hom.f (NatTrans.app (Iso.inv (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K sorry).hom
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : Hom.f (NatTrans.app (Iso.inv (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
have rw₁ : (XIsoOfEq K sorry).hom = (XIsoOfEq K sorry).hom
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := ab : Discrete ℤ }.as = n + { as := b : Discrete ℤ }.as + { as := a : Discrete ℤ }.as
have dsimp : n + ab = n + b + a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + ab = n + b + a
have rw : n + (a + b) = n + b + a
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + (a + b) = n + b + a
⊢ n + ab = n + b + a
have rw₁ : n + (a + b) = n + (b + a)
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
rw : n + (a + b) = n + b + a
rw₁ : n + (a + b) = n + (b + a)
⊢ n + ab = n + b + a
have rw₂ : n + (b + a) = n + (b + a)
Tactic: rw [← h, add_assoc, add_comm a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b ab h)) K) n =
    (XIsoOfEq K ⋯).hom
have subst : Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) sorry)) K) n =
  (XIsoOfEq K sorry).hom
Tactic: subst h
Cleared hypotheses: ab, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
have rw : Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K sorry).hom
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b n : ℤ
rw : Hom.f (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b)) K) n = (XIsoOfEq K ⋯).hom
⊢ Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) n =
    (XIsoOfEq K ⋯).hom
have rw₁ : (XIsoOfEq K sorry).hom = (XIsoOfEq K sorry).hom
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ n = n + 0
have rw : n = n
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ n + 0 = n
have rw : n = n
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
n p q : ℤ
hpq : p = q
⊢ p + n = q + n
have rw : q + n = q + n
Tactic: rw [hpq]