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 K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : ¬c.Rel j (c.next j)
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j
have neg : inrX φ j ≫ f.f j =
  CategoryStruct.comp (Y := X φ j) (inrX φ j)
    (Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      j)
Tactic: apply ext_from_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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x = y ↔
    x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
have mp : x = y →
  x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
    ∀ (i j : ι),
      c.Rel j i →
        x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
          y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
Tactic: constructor
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
mp :
  x = y →
    x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
⊢ x = y ↔
    x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
have mpr : (x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
    ∀ (i j : ι),
      c.Rel j i →
        x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
          y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j) →
  x = y
Tactic: constructor
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
    ∀ (i j : ι),
      c.Rel j i →
        x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
have mp : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
Tactic: tauto
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
mp : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
⊢ x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
    ∀ (i j : ι),
      c.Rel j i →
        x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
have mp₁ : ∀ (i j : ι),
  c.Rel j i →
    x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
      x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
Tactic: tauto
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ (x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j) →
    x = y
have mpr : ∀ (x₁ : G ⟶ K) (x₂ : Homotopy (φ ≫ x₁) 0),
  (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂) =
        y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          Homotopy.hom (f :=
              φ ≫
                Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              (g := 0)
              (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j) →
    Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂ = y
Tactic: obtain ⟨x₁, x₂⟩ := x
Cleared hypotheses: x
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
⊢ (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂) =
        y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          Homotopy.hom (f :=
              φ ≫
                Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              (g := 0)
              (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j) →
    Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂ = y
have mpr : ∀ (y₁ : G ⟶ K) (y₂ : Homotopy (φ ≫ y₁) 0),
  (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂) =
        Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
          (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) y₁ y₂) ∧
      ∀ (i j : ι),
        c.Rel j i →
          Homotopy.hom (f :=
              φ ≫
                Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              (g := 0)
              (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              i j =
            Homotopy.hom (f :=
              φ ≫
                Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) y₁ y₂))
              (g := 0)
              (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) y₁ y₂))
              i j) →
    Eq (α := (α : G ⟶ K) × Homotopy (φ ≫ α) 0) (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂)
      (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) y₁ y₂)
Tactic: obtain ⟨y₁, y₂⟩ := y
Cleared hypotheses: y
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ :
  Homotopy
    (φ ≫
      Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
    0
h :
  ∀ (i j : ι),
    c.Rel j i →
      Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          i j =
        Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
                y₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              y₂))
          i j
⊢ Eq (α := (α : G ⟶ K) × Homotopy (φ ≫ α) 0) (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂)
    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
      (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
      y₂)
have mpr : x₂ = y₂
Tactic: simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ :
  Homotopy
    (φ ≫
      Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
    0
h :
  ∀ (i j : ι),
    c.Rel j i →
      Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          i j =
        Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
                y₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              y₂))
          i j
⊢ x₂ = y₂
have mpr : ∀ (i j : ι), x₂.hom i j = y₂.hom i j
Tactic: ext 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ :
  Homotopy
    (φ ≫
      Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
    0
h :
  ∀ (i j : ι),
    c.Rel j i →
      Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          i j =
        Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
                y₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              y₂))
          i j
i j : ι
⊢ x₂.hom i j = y₂.hom i j
have pos : ∀ (hij : c.Rel j i), x₂.hom i j = y₂.hom i j
Tactic: by_cases hij : c.Rel j i
-- 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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ :
  Homotopy
    (φ ≫
      Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
    0
h :
  ∀ (i j : ι),
    c.Rel j i →
      Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
          i j =
        Homotopy.hom (f :=
          φ ≫
            Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                  (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
                y₂))
          (g := 0)
          (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) x₁ x₂))
              y₂))
          i j
i j : ι
pos : ∀ (hij : c.Rel j i), x₂.hom i j = y₂.hom i j
⊢ x₂.hom i j = y₂.hom i j
have neg : ∀ (hij : ¬c.Rel j i), x₂.hom i j = y₂.hom i j
Tactic: by_cases hij : c.Rel j i
-- 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
i j : ι
hij : c.Rel j i
⊢ inlX K i j hij ≫ Hom.f (nullHomotopicMap K) j = inlX K i j hij ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
have dsimp : CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (inlX K i j hij : K.X i ⟶ 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) =
  inlX K i j hij ≫
    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
i j : ι
hij : c.Rel j i
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 k j),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 k 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 ι
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
i j : ι
hij : c.Rel j i
pos :
  ∀ (hj : ∃ (k : ι), c.Rel k j),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inlX K i j hij : K.X i ⟶ 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) =
      inlX K i j hij ≫
        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)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 k j),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 k 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 ι
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
i j : ι
hij : c.Rel j i
hj : ∃ (k : ι), c.Rel k j
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 k j),
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ 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) =
    inlX K i j hij ≫
      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 (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 : ι
⊢ inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
have this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
Tactic: have : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr :=
    biprod.hom_ext _ _ (by simp) (by simp)
-- 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
⊢ inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
have obtain : ∀ (i : ι) (hij : c.Rel i j), inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
Tactic: obtain ⟨i, hij⟩ := hc j