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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
⊢ inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
have dsimp : CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
    (Hom.f
      (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
        homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
      j) =
  inrX K j ≫
    HSub.hSub (α :=
      homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
Tactic: dsimp [nullHomotopicMap]
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have pos : ∀ (hj : ∃ (k : ι), c.Rel j k),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
Tactic: by_cases hj : ∃ (k : ι), c.Rel j k
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
pos :
  ∀ (hj : ∃ (k : ι), c.Rel j k),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inrX K j ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have neg : ∀ (hj : ¬∃ (k : ι), c.Rel j k),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
Tactic: by_cases hj : ∃ (k : ι), c.Rel j k
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∃ (k : ι), c.Rel j k
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have pos : ∀ (k : ι) (hjk : c.Rel j k),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
Tactic: obtain ⟨k, hjk⟩ := hj
Cleared hypotheses: 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have pos : Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
  HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
    (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
Tactic: simp only [Homotopy.nullHomotopicMap'_f hij hjk,
      homotopyCofiber_X, homotopyCofiber_d, assoc, comp_add,
      homotopyCofiber.inrX_d_assoc, homotopyCofiber.inrX_sndX_assoc, comp_sub,
      inrX_π_assoc, comp_id, ← Hom.comm_assoc, homotopyCofiber.inlX_d _ _ _ _ _ hjk,
      comp_neg, add_neg_cancel_left]
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
have pos : Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
  (Iso.inv (K.biprodXIso K j) ≫
    Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
  (Iso.inv (K.biprodXIso K j) ≫
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: rw [← cancel_epi (biprodXIso K K j).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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
have pos : CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
pos :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
have pos₁ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: ext
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ (k : ι), c.Rel j k
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have hj₁ : ∀ (x : ι), ¬c.Rel j x
Tactic: simp only [not_exists] at hj
Cleared hypotheses: 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
have neg : Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
  HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
    (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
Tactic: simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj, homotopyCofiber_X,
      homotopyCofiber_d, homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc,
      comp_sub, inrX_π_assoc, comp_id, ι₀, comp_f, homotopyCofiber.inr_f]
-- 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
have neg : Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
  (Iso.inv (K.biprodXIso K j) ≫
    Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
  (Iso.inv (K.biprodXIso K j) ≫
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: rw [← cancel_epi (biprodXIso K K j).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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
have neg : CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: ext