awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
⊢ m + -1 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
simp :
  H.map
      (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
        (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
        (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n)) =
    𝟙 (H.obj ((mappingCone φ).X n))
⊢ HAdd.hAdd (α :=
        H.obj ((mappingCone φ).X n) ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (H.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n ⋯)
        (H.map (Cochain.v (snd φ) n n ⋯) ≫
          Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n) ≫
      HAdd.hAdd (α :=
        X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n ⟶
          H.obj ((mappingCone φ).X n))
        (Cochain.v
            (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
              Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
            n m ⋯ ≫
          H.map (Cochain.v (inl φ) m n ⋯))
        (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n ⋯ ≫
          H.map (Hom.f (inr φ) n)) =
    𝟙 (X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n)

Tactic:
simp only [Functor.mapHomologicalComplex_obj_X, comp_add, add_comp, assoc,
      inl_v_fst_v_assoc, inr_f_fst_v_assoc, zero_comp, comp_zero, add_zero,
      inl_v_snd_v_assoc, inr_f_snd_v_assoc, zero_add, ← Functor.map_comp, ← Functor.map_add]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_add, CategoryTheory.Functor.mapHomologicalComplex_obj_X, CochainComplex.mappingCone.inl_v_snd_v_assoc, zero_add, CategoryTheory.Preadditive.add_comp, CochainComplex.mappingCone.inr_f_fst_v_assoc, CategoryTheory.Preadditive.comp_add, CochainComplex.mappingCone.inr_f_snd_v_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp, add_zero, CochainComplex.mappingCone.inl_v_fst_v_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
rw :
  H.map
      (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
        (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
        (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n)) =
    H.map (𝟙 ((mappingCone φ).X n))
⊢ H.map
      (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
        (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
        (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n)) =
    𝟙 (H.obj ((mappingCone φ).X n))

Tactic:
rw [← H.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
e_a :
  HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
      (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n) =
    𝟙 ((mappingCone φ).X n)
⊢ H.map
      (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
        (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
        (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n)) =
    H.map (𝟙 ((mappingCone φ).X n))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
⊢ HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m ⋯ ≫ Cochain.v (inl φ) m n ⋯)
      (Cochain.v (snd φ) n n ⋯ ≫ Hom.f (inr φ) n) =
    𝟙 ((mappingCone φ).X n)

Tactic:
simp [ext_from_iff _ _ _ hnm]

Premises used: CochainComplex.mappingCone.ext_from_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
⊢ HAdd.hAdd (α :=
        X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (Cochain.v
            (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
              Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
            n m ⋯ ≫
          Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n ⋯)
        (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n ⋯ ≫
          CategoryStruct.comp (Y := H.obj (F.X m)) (H.map 0)
            (Cochain.v (inl (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) m n ⋯)) +
      HAdd.hAdd (α :=
        X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (Cochain.v
            (↑(fst (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) :
              Cochain (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))
                ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F) 1)
            n m ⋯ ≫
          CategoryStruct.comp (Y := H.obj (G.X n)) (H.map 0)
            (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n))
        (Cochain.v (snd (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n n ⋯ ≫
          Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n) =
    𝟙
      (X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)

Tactic:
simp [ext_from_iff _ _ _ hnm]

Premises used: CochainComplex.mappingCone.ext_from_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
subst :
  Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (mapHomologicalComplexXIso φ H n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (mapHomologicalComplexXIso' φ H n (n + 1) ⋯ :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
⊢ Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (mapHomologicalComplexXIso φ H n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (mapHomologicalComplexXIso' φ H n m hnm :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)

Tactic:
subst hnm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
⊢ Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (mapHomologicalComplexXIso φ H n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (mapHomologicalComplexXIso' φ H n (n + 1) ⋯ :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ)) n ≅
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
⊢ n + 1 + 1 = n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
h :
  ∀ (n : ℤ),
    Eq (α :=
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
      (Hom.f
          (CategoryStruct.comp (Y := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
            (Iso.hom (mapHomologicalComplexIso φ H)))
          n :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
      (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
        X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
          X
            (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
              (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v', u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G)
      (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (CategoryStruct.comp (Y := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
        (Iso.hom (mapHomologicalComplexIso φ H)) :
      Quiver.Hom (V := HomologicalComplex.{v', u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ) :
      Quiver.Hom (V := CochainComplex.{v', u_2, 0} D ℤ) (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G)
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
h :
  Eq (α :=
    H.obj (G.X n) ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (CategoryStruct.comp (Y := H.obj ((mappingCone φ).X n)) (H.map (Hom.f (inr φ) n))
        (Iso.hom (mapHomologicalComplexXIso φ H n)) :
      H.obj (G.X n) ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
⊢ Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (Hom.f
        (CategoryStruct.comp (Y := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
          (Iso.hom (mapHomologicalComplexIso φ H)))
        n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)

Tactic:
dsimp [mapHomologicalComplexIso]

Premises used: CochainComplex.mappingCone.mapHomologicalComplexIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
⊢ Eq (α :=
    H.obj (G.X n) ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (CategoryStruct.comp (Y := H.obj ((mappingCone φ).X n)) (H.map (Hom.f (inr φ) n))
        (Iso.hom (mapHomologicalComplexXIso φ H n)) :
      H.obj (G.X n) ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)

Tactic:
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl, mappingCone.ext_to_iff _ _ _ rfl,
    Functor.mapHomologicalComplex_obj_X, mapHomologicalComplexXIso'_hom, comp_add,
    add_comp, assoc, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero, add_zero, inl_v_snd_v,
    inr_f_snd_v, zero_add, ← H.map_comp, H.map_zero, H.map_id, and_self]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inr_f_fst_v, and_self, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.mapHomologicalComplex_obj_X, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.mappingCone.ext_to_iff, CategoryTheory.Category.comp_id, zero_add, CochainComplex.mappingCone.mapHomologicalComplexXIso_eq, CochainComplex.mappingCone.inl_v_fst_v, CategoryTheory.Preadditive.add_comp, HAdd.hAdd, CategoryTheory.Functor.map_id, CategoryTheory.Preadditive.comp_add, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, CategoryTheory.Functor.map_comp, CochainComplex.mappingCone.inl_v_snd_v, add_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
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 : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
obtain : ∀ (n : ℤ) (hn : K.IsStrictlyGE n), CochainComplex.plus C (cylinder K)
⊢ CochainComplex.plus C (cylinder K)

Tactic:
obtain ⟨n, hn⟩ := hK
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ CochainComplex.plus C (cylinder K)

Tactic:
⟨n - 1, ?_⟩

Premises used: HSub.hSub, Exists.intro, CochainComplex.plus, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
refine : IsStrictlyGE (cylinder K) (n - 1)
⊢ CochainComplex.plus C (cylinder K)

Tactic:
refine ⟨n - 1, ?_⟩