awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ (triangle φ).rotate ≅ mappingCone.triangle φ
have refine : (triangle φ).rotate.mor₃ ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
      (Iso.hom (Iso.refl (triangle φ).rotate.obj₁)) =
  Iso.hom
      (Iso.app (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2) (mappingCone φ)) ≫
    (mappingCone.triangle φ).mor₃
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    ((shiftFunctorCompIsoId _ (-1 : ℤ) 1 (by lia)).app _)
    (by simp) (by simp [triangle]) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ (triangle φ).rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangle φ).rotate.obj₁)) =
    Iso.hom
        (Iso.app (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2) (mappingCone φ)) ≫
      (mappingCone.triangle φ).mor₃
have dsimp : (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (fst φ)) ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K) =
  NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
      (mappingCone φ) ≫
    (mappingCone.triangle φ).mor₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (fst φ)) ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K) =
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
        (mappingCone φ) ≫
      (mappingCone.triangle φ).mor₃
have h : ∀ (n : ℤ),
  Hom.f
      ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
            (fst φ)) ≫
        CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K))
      n =
    Hom.f
      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
          (mappingCone φ) ≫
        (mappingCone.triangle φ).mor₃)
      n
Tactic: ext n
-- 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 φ
i : ℤ
⊢ IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (F.X (i + 1)) ∧ IsZero.{v, u_1} (G.X i)
have this : HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)
Tactic: have := HasHomotopyCofiber.hasBinaryBiproduct φ i (i + 1) rfl
-- 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 φ
i : ℤ
this : HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)
⊢ IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (F.X (i + 1)) ∧ IsZero.{v, u_1} (G.X i)
have rw : IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (biprod.{v, u_1} (F.X (i + 1)) (G.X i))
Tactic: rw [← biprod_isZero_iff]
-- 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 φ
⊢ Eq.{v + 1} (α := Cochain (mappingCone φ) F 2)
    (δ 1 2 (Cochain.mk fun (p q : ℤ) (hpq : p + 1 = q) ↦ homotopyCofiber.fstX φ p q hpq)) 0
have h : ∀ (p : ℤ),
  Eq.{v + 1} (α := (mappingCone φ).X p ⟶ F.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (hpq : p + 1 = q) ↦ homotopyCofiber.fstX φ p q hpq)) p (p + 2) sorry)
    (Cochain.v 0 p (p + 2) sorry)
Tactic: ext p _ rfl
-- 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 φ
p q : ℤ
hpq : q + 1 = p
⊢ p + -1 = q
have rw : q + 1 + -1 = q
Tactic: rw [← hpq, add_neg_cancel_right]
-- 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 φ
p q : ℤ
hpq : q + 1 = p
rw : q + 1 + -1 = q
⊢ p + -1 = q
have rw₁ : q = q
Tactic: rw [← hpq, add_neg_cancel_right]
-- 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 φ
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ = Cochain.ofHom (𝟙 F)
have h : ∀ (p : ℤ),
  (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) sorry).v p p sorry =
    (Cochain.ofHom (𝟙 F)).v p p sorry
Tactic: ext p
-- 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 φ
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯ = 0
have h : ∀ (p q : ℤ) (hpq : p + -1 = q), (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) sorry).v p q hpq = Cochain.v 0 p q hpq
Tactic: ext
-- 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 φ
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ = 0
have h : ∀ (p q : ℤ) (hpq : p + 1 = q),
  (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) sorry).v p q hpq =
    Cochain.v 0 p q hpq
Tactic: ext
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ -1 + e = d
have rw : -1 + (1 + d) = d
Tactic: rw [← he, 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
rw : -1 + (1 + d) = d
⊢ -1 + e = d
have rw₁ : d = d
Tactic: rw [← he, 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he) ⋯ = γ
have rw : (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) sorry).comp γ sorry = γ
Tactic: rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ ⋯ = γ
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he) ⋯ = γ
have rw₁ : (Cochain.ofHom (𝟙 F)).comp γ sorry = γ
Tactic: rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ ⋯ = γ
rw₁ : (Cochain.ofHom (𝟙 F)).comp γ ⋯ = γ
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he) ⋯ = γ
have rw₂ : γ = γ
Tactic: rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]
-- 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 ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
have obtain : ∀ (γ : Cochain G K e) (he : 0 + e = e), Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
Tactic: obtain rfl : e = d := by lia
Cleared hypotheses: d, γ, he
-- 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 ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
have rw : (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) sorry).comp γ hf = 0
Tactic: rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]
-- 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 ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯).comp γ hf = 0
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
have rw₁ : Eq (α := Cochain F K f) (Cochain.comp 0 γ hf) 0
Tactic: rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]
-- 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 ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
rw : (Cochain.comp (G := mappingCone φ) (inl φ) (snd φ) ⋯).comp γ hf = 0
rw₁ : Eq (α := Cochain F K f) (Cochain.comp 0 γ hf) 0
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.comp (snd φ) γ he) hf = 0
have rw₂ : Eq.{v + 1} (α := Cochain F K f) 0 0
Tactic: rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]
-- 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 ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0
have obtain : ∀ (hf : 0 + e = e),
  Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0
Tactic: obtain rfl : e = f := by lia
Cleared hypotheses: f, hf
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0
have rw : (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) sorry).comp γ he = 0
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_fst, Cochain.zero_comp]
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
rw :
  (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ he = 0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0
have rw₁ : Eq (α := Cochain G K e) (Cochain.comp 0 γ he) 0
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_fst, Cochain.zero_comp]
-- 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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
rw :
  (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯).comp γ he = 0
rw₁ : Eq (α := Cochain G K e) (Cochain.comp 0 γ he) 0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) γ he)
      hf =
    0
have rw₂ : Eq.{v + 1} (α := Cochain G K e) 0 0
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_fst, Cochain.zero_comp]
-- 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 ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ
have obtain : ∀ (he : 0 + d = d), Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) sorry = γ
Tactic: obtain rfl : d = e := by lia
Cleared hypotheses: e, he
-- 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 ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ
have rw : (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (snd φ) sorry).comp γ he = γ
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]
-- 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 ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
rw : (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (snd φ) ⋯).comp γ he = γ
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ
have rw₁ : (Cochain.ofHom (𝟙 G)).comp γ he = γ
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]
-- 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 ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
rw : (Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (snd φ) ⋯).comp γ he = γ
rw₁ : (Cochain.ofHom (𝟙 G)).comp γ he = γ
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (Cochain.comp (snd φ) γ he) ⋯ = γ
have rw₂ : γ = γ
Tactic: rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]
-- 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 φ
i j : ℤ
hij : i + 1 = j
A : C
f g : A ⟶ (mappingCone φ).X i
⊢ f = g ↔
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
have mp : f = g →
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
      g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
    f ≫ Cochain.v (snd φ) i i sorry = g ≫ Cochain.v (snd φ) i i sorry
Tactic: constructor
-- 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 φ
i j : ℤ
hij : i + 1 = j
A : C
f g : A ⟶ (mappingCone φ).X i
mp :
  f = g →
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
⊢ f = g ↔
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
        g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
      f ≫ Cochain.v (snd φ) i i ⋯ = g ≫ Cochain.v (snd φ) i i ⋯
have mpr : f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
      g ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
    f ≫ Cochain.v (snd φ) i i sorry = g ≫ Cochain.v (snd φ) i i sorry →
  f = g
Tactic: constructor
-- 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 φ
i j : ℤ
hij : i + 1 = j
A : C
f : A ⟶ (mappingCone φ).X i
⊢ f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
      f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
    f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯
have mp : f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
Tactic: tauto
-- 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 φ
i j : ℤ
hij : i + 1 = j
A : C
f : A ⟶ (mappingCone φ).X i
mp :
  f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
    f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
⊢ f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
      f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ∧
    f ≫ Cochain.v (snd φ) i i ⋯ = f ≫ Cochain.v (snd φ) i i ⋯
have mp₁ : f ≫ Cochain.v (snd φ) i i sorry = f ≫ Cochain.v (snd φ) i i sorry
Tactic: tauto
-- 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 φ
i j : ℤ
hij : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
⊢ f = g ↔ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
have mp : f = g → Cochain.v (inl φ) i j sorry ≫ f = Cochain.v (inl φ) i j sorry ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
Tactic: constructor
-- 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 φ
i j : ℤ
hij : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
mp : f = g → Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
⊢ f = g ↔ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g
have mpr : Cochain.v (inl φ) i j sorry ≫ f = Cochain.v (inl φ) i j sorry ≫ g ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ g → f = g
Tactic: constructor
-- 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 φ
i j : ℤ
hij : j + 1 = i
A : C
f : (mappingCone φ).X j ⟶ A
⊢ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
have mp : Cochain.v (inl φ) i j sorry ≫ f = Cochain.v (inl φ) i j sorry ≫ f
Tactic: tauto
-- 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 φ
i j : ℤ
hij : j + 1 = i
A : C
f : (mappingCone φ).X j ⟶ A
mp : Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f
⊢ Cochain.v (inl φ) i j ⋯ ≫ f = Cochain.v (inl φ) i j ⋯ ≫ f ∧ Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
have mp₁ : Hom.f (inr φ) j ≫ f = Hom.f (inr φ) j ≫ f
Tactic: tauto
-- 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 φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f =
    HAdd.hAdd (α := A ⟶ (mappingCone φ).X i)
      ((f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij) ≫ Cochain.v (inl φ) j i ⋯)
      ((f ≫ Cochain.v (snd φ) i i ⋯) ≫ Hom.f (inr φ) i)
have h₁ : f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij =
  HAdd.hAdd (α := A ⟶ (mappingCone φ).X i)
      ((f ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij) ≫ Cochain.v (inl φ) j i sorry)
      ((f ≫ Cochain.v (snd φ) i i sorry) ≫ Hom.f (inr φ) i) ≫
    Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij
Tactic: apply ext_to φ i j hij