awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
rw : 1 + m = m + 1
⊢ 1 + m = n
have rw₁ : m + 1 = m + 1
Tactic: rw [← h, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + m = p₃
have rw : p₁ + m = p₂ + n
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
⊢ p₁ + m = p₃
have rw₁ : p₁ + m = p₁ + -1 + n
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
rw₁ : p₁ + m = p₁ + -1 + n
⊢ p₁ + m = p₃
have rw₂ : p₁ + m = p₁ + -1 + (m + 1)
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
rw₁ : p₁ + m = p₁ + -1 + n
rw₂ : p₁ + m = p₁ + -1 + (m + 1)
⊢ p₁ + m = p₃
have rw₃ : p₁ + m = p₁ + -1 + (1 + m)
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
rw₁ : p₁ + m = p₁ + -1 + n
rw₂ : p₁ + m = p₁ + -1 + (m + 1)
rw₃ : p₁ + m = p₁ + -1 + (1 + m)
⊢ p₁ + m = p₃
have rw₄ : p₁ + m = p₁ + (-1 + (1 + m))
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
rw₁ : p₁ + m = p₁ + -1 + n
rw₂ : p₁ + m = p₁ + -1 + (m + 1)
rw₃ : p₁ + m = p₁ + -1 + (1 + m)
rw₄ : p₁ + m = p₁ + (-1 + (1 + m))
⊢ p₁ + m = p₃
have rw₅ : p₁ + m = p₁ + m
Tactic: rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ n n'
      (HAdd.hAdd (α := Cochain (mappingCone φ) K n) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) α ⋯)
        (Cochain.comp (snd φ) β ⋯)) =
    HAdd.hAdd (α := Cochain (mappingCone φ) K n')
      (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
      (Cochain.comp (snd φ) (δ n n' β) ⋯)
have simp : Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) sorry +
    (Cochain.comp (snd φ) (δ n n' β) sorry +
      -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
          (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β sorry) sorry)) =
  Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) sorry +
      -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
          (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β sorry) sorry) +
    Cochain.comp (snd φ) (δ n n' β) sorry
Tactic: simp only [δ_add, Cochain.comp_add, δ_comp (fst φ).1 α _ 2 n n' hn' (by lia) (by lia),
    Cocycle.δ_eq_zero, Cochain.zero_comp, smul_zero, add_zero,
    δ_comp (snd φ) β (zero_add n) 1 n' n' hn' (zero_add 1) hn', δ_snd, Cochain.neg_comp,
    smul_neg, Cochain.comp_assoc_of_second_is_zero_cochain, Cochain.comp_units_smul, ← hn',
    Int.negOnePow_succ, Units.neg_smul, Cochain.comp_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  Cochain.comp (inl φ) (Cochain.ofHom f₁) ⋯ =
    δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + Cochain.comp (inl φ) (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ Cochain.ofHom f₁ = δ (-1) 0 (descCochain φ γ₁ γ₂ descHomotopy._proof_1) + Cochain.ofHom f₂
have h₃ : Cochain.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₁) sorry =
  δ (-1) 0 γ₂ + Cochain.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₂) sorry
Tactic: simp only [Cochain.ofHom_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
m' : ℤ
hm' : m + 1 = m'
⊢ δ n m (HAdd.hAdd (α := Cochain K (mappingCone φ) n) (α.comp (inl φ) ⋯) (β.comp (Cochain.ofHom (inr φ)) ⋯)) =
    HAdd.hAdd (α := Cochain K (mappingCone φ) m) (-(δ m m' α).comp (inl φ) ⋯)
      ((δ n m β + α.comp (Cochain.ofHom φ) ⋯).comp (Cochain.ofHom (inr φ)) ⋯)
have simp : HAdd.hAdd (α := Cochain K (mappingCone φ) m) (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) sorry) sorry)
      (-(δ m m' α).comp (inl φ) sorry) +
    (δ n m β).comp (Cochain.ofHom (inr φ)) sorry =
  -(δ m m' α).comp (inl φ) sorry +
    HAdd.hAdd (α := Cochain K (mappingCone φ) m) ((δ n m β).comp (Cochain.ofHom (inr φ)) sorry)
      (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) sorry) sorry)
Tactic: simp only [δ_add, δ_comp α (inl φ) _ m' _ _ h hm' (neg_add_cancel 1),
    δ_comp_zero_cochain _ _ _ h, δ_inl, Cochain.ofHom_comp,
    Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
    δ_ofHom, Cochain.comp_zero, zero_add, Cochain.add_comp,
    Cochain.comp_assoc_of_second_is_zero_cochain]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (lift φ α β eq) p) (Cochain.v (snd φ) p q hpq) = β.v p q hpq
have obtain : ∀ (hpq : q + 0 = q),
  CategoryStruct.comp (Y := (mappingCone φ).X q) (Hom.f (lift φ α β eq) q) (Cochain.v (snd φ) q q hpq) = β.v q q hpq
Tactic: obtain rfl : q = p := by lia
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ m + -1 + n' = p
have linarith : m + -1 + n' < p → -1 + (n + 1 - m) + -(n + n' - p) + (m + -1 + n' + 1 - p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
linarith : m + -1 + n' < p → -1 + (n + 1 - m) + -(n + n' - p) + (m + -1 + n' + 1 - p) = 0
⊢ m + -1 + n' = p
have linarith₁ : p < m + -1 + n' → -1 + -(n + 1 - m) + (n + n' - p) + (p + 1 - (m + -1 + n')) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
K L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (descCochain φ α' β' h') p₂ p₃ h₂₃) =
    α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃
have eq : (Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (descCochain φ α' β' h') hp).v p₁ p₃ sorry =
  (α.comp α' sorry + β.comp β' sorry).v p₁ p₃ sorry
Tactic: have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 (α :=
        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)
have simp : H.map
    (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m sorry ≫ Cochain.v (inl φ) m n sorry)
      (Cochain.v (snd φ) n n sorry ≫ Hom.f (inr φ) n)) =
  𝟙 (H.obj ((mappingCone φ).X 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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
⊢ 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))
have rw : H.map
    (HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m sorry ≫ Cochain.v (inl φ) m n sorry)
      (Cochain.v (snd φ) n n sorry ≫ Hom.f (inr φ) n)) =
  H.map (𝟙 ((mappingCone φ).X n))
Tactic: rw [← H.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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
⊢ 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))
have e_a : HAdd.hAdd (α := (mappingCone φ).X n ⟶ (mappingCone φ).X n)
    (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) n m sorry ≫ Cochain.v (inl φ) m n sorry)
    (Cochain.v (snd φ) n n sorry ≫ Hom.f (inr φ) n) =
  𝟙 ((mappingCone φ).X n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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
⊢ 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)
have 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) sorry :
    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
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
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 ℤ)) φ)
⊢ 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 ℤ)) φ)))
have 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)
Tactic: ext n