awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
⊢ f = g
have rw : Eq (α := A ⟶ biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij))
  (g ≫ Iso.hom (XIsoBiprod φ i j hij))
Tactic: rw [← cancel_mono (XIsoBiprod φ i j hij).hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
⊢ Eq (α := A ⟶ biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij))
    (g ≫ Iso.hom (XIsoBiprod φ i j hij))
have h₀ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst
Tactic: apply biprod.hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst
⊢ Eq (α := A ⟶ biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij))
    (g ≫ Iso.hom (XIsoBiprod φ i j hij))
have h₃ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd
Tactic: apply biprod.hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd
have h₃ : ∀ (hij : c.Rel i (c.next i)) (h₁ : f ≫ fstX φ i (c.next i) hij = g ≫ fstX φ i (c.next i) hij)
  (this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)),
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij))
      biprod.snd =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij))
      biprod.snd
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hij, h₁, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g
have rw : f ≫ Iso.hom (XIso φ i hi) = g ≫ Iso.hom (XIso φ i hi)
Tactic: rw [← cancel_mono (XIso φ i hi).hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
⊢ f = g
have this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
Tactic: haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
⊢ f = g
have rw : Eq (α := biprod.{v_1, u_1} (F.X i) (G.X j) ⟶ A) (Iso.inv (XIsoBiprod φ j i hij) ≫ f)
  (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
Tactic: rw [← cancel_epi (XIsoBiprod φ j i hij).inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
⊢ Eq (α := biprod.{v_1, u_1} (F.X i) (G.X j) ⟶ A) (Iso.inv (XIsoBiprod φ j i hij) ≫ f)
    (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
have h₀ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
Tactic: apply biprod.hom_ext'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
⊢ Eq (α := biprod.{v_1, u_1} (F.X i) (G.X j) ⟶ A) (Iso.inv (XIsoBiprod φ j i hij) ≫ f)
    (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
have h₃ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
Tactic: apply biprod.hom_ext'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
have h₃ : ∀ (hij : c.Rel j (c.next j)) (h₁ : inlX φ (c.next j) j hij ≫ f = inlX φ (c.next j) j hij ≫ g)
  (this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next j)) (G.X j)),
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
      (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
      (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ g)
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: i, hij, h₁, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ f = g
have rw : Iso.inv (XIso φ i hi) ≫ f = Iso.inv (XIso φ i hi) ≫ g
Tactic: rw [← cancel_epi (XIso φ i hi).inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq (α := X φ i ⟶ F.X k) (d φ i j ≫ fstX φ j k hjk) (-fstX φ i j hij ≫ F.d j k)
have obtain : ∀ (hjk : c.Rel j (c.next j)),
  Eq (α := X φ i ⟶ F.X (c.next j)) (d φ i j ≫ fstX φ j (c.next j) hjk) (-fstX φ i j hij ≫ F.d j (c.next j))
Tactic: obtain rfl := c.next_eq' hjk
Cleared hypotheses: k, hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ d φ i j ≫ sndX φ j = HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
have dsimp : CategoryStruct.comp (Y := X φ j)
    (if hij : c.Rel i j then
      HAdd.hAdd (α := X φ i ⟶ X φ j)
          (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0)
          (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
        sndX φ i ≫ G.d i j ≫ inrX φ j
    else 0)
    (sndX φ j) =
  HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
Tactic: dsimp [d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ CategoryStruct.comp (Y := X φ j)
      (if hij : c.Rel i j then
        HAdd.hAdd (α := X φ i ⟶ X φ j)
            (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0)
      (sndX φ j) =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
have pos : ∀ (hij_1 : c.Rel j (c.next j)),
  (HAdd.hAdd (α := X φ i ⟶ X φ j) (-fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij_1)
          (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
        sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
      sndX φ j =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
Tactic: split_ifs with hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
pos :
  ∀ (hij_1 : c.Rel j (c.next j)),
    (HAdd.hAdd (α := X φ i ⟶ X φ j) (-fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij_1)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
        sndX φ j =
      HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
⊢ CategoryStruct.comp (Y := X φ j)
      (if hij : c.Rel i j then
        HAdd.hAdd (α := X φ i ⟶ X φ j)
            (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0)
      (sndX φ j) =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
have neg : ∀ (hij_1 : ¬c.Rel j (c.next j)),
  (HAdd.hAdd (α := X φ i ⟶ X φ j) 0 (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ sndX φ j =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
Tactic: split_ifs with hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ inlX φ j i hij ≫ d φ i j = HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j)
have h₁ : CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (fstX φ j k hjk) =
  HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk
Tactic: apply ext_to_X φ j k hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h₁ :
  CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (fstX φ j k hjk) =
    HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk
⊢ inlX φ j i hij ≫ d φ i j = HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j)
have h₂ : CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
  HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ sndX φ j
Tactic: apply ext_to_X φ j k hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ Eq (α := F.X j ⟶ X φ j) (inlX φ j i hij ≫ d φ i j) (φ.f j ≫ inrX φ j)
have apply : CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
  CategoryStruct.comp (Y := X φ j) (φ.f j ≫ inrX φ j) (sndX φ j)
Tactic: apply ext_to_X' _ _ hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have pos : ∀ (hij : c.Rel i j), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
pos : ∀ (hij : c.Rel i j), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg : ∀ (hij : ¬c.Rel i j), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have pos : ∀ (hj : c.Rel j (c.next j)), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
Tactic: by_cases hj : c.Rel j (c.next j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
pos : ∀ (hj : c.Rel j (c.next j)), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg : ∀ (hj : ¬c.Rel j (c.next j)), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
Tactic: by_cases hj : c.Rel j (c.next j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have pos : CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (fstX φ j (c.next j) hj) =
  CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (fstX φ j (c.next j) hj)
Tactic: apply ext_to_X _ _ _ hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
pos :
  CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (fstX φ j (c.next j) hj) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (fstX φ j (c.next j) hj)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have pos₁ : CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
  CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)
Tactic: apply ext_to_X _ _ _ hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg : CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
  CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)
Tactic: apply ext_to_X' _ _ hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (G.d i j ≫ inrX φ j)
Tactic: rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
neg : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (G.d i j ≫ inrX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg₁ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (0 ≫ inrX φ j)
Tactic: rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
neg : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (G.d i j ≫ inrX φ j)
neg₁ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (0 ≫ inrX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg₂ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) 0
Tactic: rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
neg : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (G.d i j ≫ inrX φ j)
neg₁ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (0 ≫ inrX φ j)
neg₂ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) 0
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
have neg₃ : Eq.{v_1 + 1} (α := G.X i ⟶ X φ j) 0 0
Tactic: rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq (α := homotopyCofiber.X φ i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k) 0
have h₁ : Eq (α := F.X j ⟶ homotopyCofiber.X φ k)
  (homotopyCofiber.inlX φ j i hij ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
  (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inlX φ j i hij) 0)
Tactic: apply homotopyCofiber.ext_from_X φ j i hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h₁ :
  Eq (α := F.X j ⟶ homotopyCofiber.X φ k)
    (homotopyCofiber.inlX φ j i hij ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
    (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inlX φ j i hij) 0)
⊢ Eq (α := homotopyCofiber.X φ i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k) 0
have h₂ : Eq (α := G.X i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.inrX φ i ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
  (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inrX φ i) 0)
Tactic: apply homotopyCofiber.ext_from_X φ j i hij