awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : Plus.{v_1, u_1} C
⊢ ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K
have obtain : ∀ (L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ))
  (hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)),
  ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K
Tactic: obtain ⟨L, hL⟩ := HomotopyCategory.quotient_obj_surjective K.obj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) = K
have obj : (Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)).obj (P := plus C) =
  K.obj (P := plus C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K
have refine : CochainComplex.plus C L
Tactic: refine ⟨⟨L, ?_⟩, by ext; exact hL⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ CochainComplex.plus C L
have rw : plus C (K.obj (P := plus C))
Tactic: rw [← HomotopyCategory.plus_quotient_obj_iff, hL]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
K : Plus.{v_1, u_1} C
⊢ Functor.essImage (quotient C) K
have obtain : ∀ (L : CochainComplex.Plus.{v_1, u_1} C), Functor.essImage (quotient C) (Functor.obj (quotient C) L)
Tactic: obtain ⟨L, rfl⟩ := quotient_obj_surjective K
Cleared hypotheses: K
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K ⟶ L
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L) (CategoryTheory.Functor.map (quotient C) f₀)
    (CategoryTheory.Functor.map (quotient C) f₁)
⊢ ∃ (P : Precylinder K) (x : P.LeftHomotopy f₀ f₁),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
have obtain : ∀ (f₀ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C))
  (hf :
    Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
      (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
      (CategoryTheory.Functor.map (quotient C) f₁)),
  ∃ (P : Precylinder K) (x : P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀) f₁),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
Tactic: obtain ⟨f₀, rfl⟩ := ObjectProperty.homMk_surjective f₀
Cleared hypotheses: f₀, hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₁ : K ⟶ L
f₀ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
    (CategoryTheory.Functor.map (quotient C) f₁)
⊢ ∃ (P : Precylinder K) (x : P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀) f₁),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
have obtain : ∀ (f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C))
  (hf :
    Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
      (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
      (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₁))),
  ∃ (P : Precylinder K) (x :
    P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
      (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
Tactic: obtain ⟨f₁, rfl⟩ := ObjectProperty.homMk_surjective f₁
Cleared hypotheses: f₁, hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₁))
⊢ ∃ (P : Precylinder K) (x :
    P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
      (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
have replace : ∀ (hf : Homotopy f₀ f₁),
  ∃ (P : Precylinder K) (x :
    P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
      (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
Tactic: replace hf := homotopyOfEq f₀ f₁ ((HomotopyCategory.Plus.ι _).congr_map hf)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
X : C
⊢ plus.{v_1, u_1} C (Functor.obj (singleFunctor C n) X)
have rw : CochainComplex.plus.{v_1, u_1} C (Functor.obj (CochainComplex.singleFunctor C n) X)
Tactic: rw [← quotient_obj_singleFunctors_obj, plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ p = q + 1
have rw : p = p + -1 + 1
Tactic: rw [← hpq, neg_add_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
rw : p = p + -1 + 1
⊢ p = q + 1
have rw₁ : p = p
Tactic: rw [← hpq, neg_add_cancel_right]
-- 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ Cochain.v (inl φ) p q hpq ≫ (triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv
have dsimp : CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q hpq)
    (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) q q sorry) =
  -(HomologicalComplex.XIsoOfEq K sorry).inv
Tactic: dsimp [triangle]
-- 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
⊢ HomologicalComplex.Hom.f (inr φ) p ≫ (triangle φ).mor₃.f p = 0
have dsimp : CategoryStruct.comp (Y := (mappingCone φ).X p) (HomologicalComplex.Hom.f (inr φ) p)
    (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) p p sorry) =
  0
Tactic: dsimp [triangle]
-- 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ inr φ ≫ (triangle φ).mor₃ = 0
have h : ∀ (i : ℤ), (inr φ ≫ (triangle φ).mor₃).f i = HomologicalComplex.Hom.f 0 i
Tactic: ext
-- 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
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ mapOfHomotopy H ≫ (triangle φ₂).mor₃ =
    (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a
have h : ∀ (p : ℤ),
  HomologicalComplex.Hom.f (mapOfHomotopy H ≫ (triangle φ₂).mor₃) p =
    ((triangle φ₁).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a).f
      p
Tactic: ext p
-- 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
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ HomologicalComplex.Hom.f (mapOfHomotopy H ≫ (triangle φ₂).mor₃) p =
    ((triangle φ₁).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a).f
      p
have h : Eq (α := (mappingCone φ₁).X p ⟶ K₂.X (p + 1))
  (HomologicalComplex.Hom.f
      (desc φ₁
        (HAdd.hAdd (α := Cochain K₁ (mappingCone φ₂) (-1)) ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy._proof_2)
          ((Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy._proof_3))
        (b ≫ inr φ₂) sorry)
      p ≫
    Cochain.v (Cochain.rightShift (-(↑(fst φ₂) : Cochain (mappingCone φ₂) K₂ 1)) 1 0 triangle._proof_3) p p sorry)
  (Cochain.v (Cochain.rightShift (-(↑(fst φ₁) : Cochain (mappingCone φ₁) K₁ 1)) 1 0 triangle._proof_3) p p sorry ≫
    a.f (p + 1))
Tactic: dsimp [mapOfHomotopy, triangle]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α := (triangleh φ₁).obj₁ ⟶ (triangleh φ₂).obj₂)
    ((triangleh φ₁).mor₁ ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫ (triangleh φ₂).mor₁)
have dsimp : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₁ ≫
    CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫
    CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₁ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₂)
have simp : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (φ₁ ≫ b))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (a ≫ φ₂))
Tactic: simp only [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α := (triangleh φ₁).obj₂ ⟶ (triangleh φ₂).obj₃)
    ((triangleh φ₁).mor₂ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b ≫ (triangleh φ₂).mor₂)
have dsimp : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
  (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₁) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂)) :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₂) :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (triangleh φ₁).mor₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a) =
    CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ (triangleh φ₂).mor₃
have dsimp : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂))
  ((CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₁) ≫
    CategoryTheory.Functor.map
      (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a))
  (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₂).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₂ :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂) ⟶
        Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
⊢ φ ≫ 𝟙 L = 𝟙 K ≫ φ
have rw : φ ≫ 𝟙 L = φ
Tactic: rw [id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
rw : φ ≫ 𝟙 L = φ
⊢ φ ≫ 𝟙 L = 𝟙 K ≫ φ
have rw₁ : φ = φ
Tactic: rw [id_comp, comp_id]
-- 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
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ Eq (α := mappingCone φ ⟶ mappingCone φ) (map φ φ (𝟙 K) (𝟙 L) ⋯ : mappingCone φ ⟶ mappingCone φ)
    (𝟙 (mappingCone φ) : mappingCone φ ⟶ mappingCone φ)
have h : ∀ (n : ℤ), HomologicalComplex.Hom.f (map φ φ (𝟙 K) (𝟙 L) sorry) n = HomologicalComplex.Hom.f (𝟙 (mappingCone φ)) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃
have rw : a ≫ φ₂ ≫ b' = (a ≫ a') ≫ φ₃
Tactic: rw [reassoc_of% comm, comm', assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
rw : a ≫ φ₂ ≫ b' = (a ≫ a') ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃
have rw₁ : a ≫ a' ≫ φ₃ = (a ≫ a') ≫ φ₃
Tactic: rw [reassoc_of% comm, comm', assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
rw : a ≫ φ₂ ≫ b' = (a ≫ a') ≫ φ₃
rw₁ : a ≫ a' ≫ φ₃ = (a ≫ a') ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃
have rw₂ : a ≫ a' ≫ φ₃ = a ≫ a' ≫ φ₃
Tactic: rw [reassoc_of% comm, comm', assoc]