awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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)
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
mp₂ mp₃ mp₄ : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
mp₅ mp₆ 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
mp₈ mp₉ mp₁₀ : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
mp₁₁ mp₁₂ 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
mp₁₄ mp₁₅ mp₁₆ : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
mp₁₇ mp₁₈ 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
mp₂₀ : x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
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
⊢ 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

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
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
⊢ (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:
obtain ⟨x₁, x₂⟩ := x
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
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₂)
⊢ (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 ⟨y₁, y₂⟩ := y
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
mpr : x₂ = y₂
⊢ 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₂)

Tactic:
simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]

Premises used: heq_eq_eq, Sigma.mk.inj_iff, true_and
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
mpr : ∀ (i j : ι), x₂.hom i j = y₂.hom i j
⊢ x₂ = y₂

Tactic:
ext i j
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
neg : ∀ (hij : ¬c.Rel j i), x₂.hom i j = y₂.hom i j
⊢ x₂.hom i j = y₂.hom i j

Tactic:
by_cases hij : c.Rel j i

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 : ι
hij : c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
h _ _ hij
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 : ι
hij : c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
exact h _ _ hij
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
simp only [Homotopy.zero _ _ _ hij]

Premises used: Homotopy.zero
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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_1 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
K : HomologicalComplex.{v_1, u_1, u_2} C c
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
f : homotopyCofiber φ ⟶ K
⊢ φ ≫ inr φ ≫ f = (φ ≫ inr φ) ≫ f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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_1 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
K : HomologicalComplex.{v_1, u_1, u_2} C c
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
f : homotopyCofiber φ ⟶ K
⊢ Eq (α := F ⟶ K) (0 ≫ f) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
inst_4 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_5 : K.HasCylinder
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ CategoryStruct.comp (Y := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) (biprod.desc φ₀ φ₁) = φ₀ - φ₁

Tactic:
simp only [biprod.lift_desc, id_comp, neg_comp, sub_eq_add_neg]

Premises used: sub_eq_add_neg, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Limits.biprod.lift_desc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 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
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ CategoryStruct.comp (Y := K.cylinder) (ι₀ K) (desc φ₀ φ₁ h) = φ₀

Tactic:
simp [ι₀, desc]

Premises used: HomologicalComplex.cylinder.desc, HomologicalComplex.cylinder.ι₀
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 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
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ CategoryStruct.comp (Y := K.cylinder) (ι₁ K) (desc φ₀ φ₁ h) = φ₁

Tactic:
simp [ι₁, desc]

Premises used: HomologicalComplex.cylinder.desc, HomologicalComplex.cylinder.ι₁
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
⊢ CategoryStruct.comp (Y := K.cylinder) (ι₀ K) (π K) = 𝟙 K

Tactic:
simp [π]

Premises used: HomologicalComplex.cylinder.π
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
⊢ CategoryStruct.comp (Y := K.cylinder) (ι₁ K) (π K) = 𝟙 K

Tactic:
simp [π]

Premises used: HomologicalComplex.cylinder.π
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 := K.cylinder.X j) (inlX K i j hij) (Hom.f (π K) j) = 0

Tactic:
simp [HomologicalComplex.cylinder.π, HomologicalComplex.cylinder.desc, Homotopy.equivSubZero]

Premises used: HomologicalComplex.cylinder.desc, Homotopy.equivSubZero, HomologicalComplex.cylinder.π
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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 : ι
⊢ Eq (α := (K ⊞ K).X i ⟶ K.X i)
    (CategoryStruct.comp (Y := K.cylinder.X i) (inrX K i) (Hom.f (π K) i) : (K ⊞ K).X i ⟶ K.X i)
    (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) i : (K ⊞ K).X i ⟶ K.X i)

Tactic:
homotopyCofiber.inrX_desc_f _ _ _ _

Premises used: HomologicalComplex.homotopyCofiber.X, HomologicalComplex.homotopyCofiber.inrX_desc_f, dite
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
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
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))
⊢ inlX K i j hij ≫ Hom.f (nullHomotopicMap K) j = inlX K i j hij ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j

Tactic:
dsimp [nullHomotopicMap]

Premises used: HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap