awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))

Tactic:
(I K).isZero_of_isStrictlyGE (n + 1) _

Premises used: CochainComplex.cm5b.I, CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, CategoryTheory.Injective.under, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))

Tactic:
exact (I K).isZero_of_isStrictlyGE (n + 1) _

Premises used: CochainComplex.cm5b.I, CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
h :
  ∀ (p q : ℤ) (hpq : p + 2 = q),
    Eq.{v_1 + 1} (α := K.X p ⟶ (I K).X q)
      (HomComplex.Cochain.v
        (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ K.d p q ≫ Injective.ι (K.X q))) p q
        hpq)
      (HomComplex.Cochain.v 0 p q hpq)
⊢ Eq.{v_1 + 1} (α := HomComplex.Cochain K (I K) 2)
    (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ K.d p q ≫ Injective.ι (K.X q))) 0

Tactic:
ext p q hpq

Premises used: CochainComplex.cm5b.p
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
p q : ℤ
hpq : p + 2 = q
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
p q : ℤ
hpq : p + 2 = q
⊢ p + 1 = q - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
p q : ℤ
hpq : p + 2 = q
⊢ Eq.{v_1 + 1} (α := K.X p ⟶ (I K).X q)
    (HomComplex.Cochain.v
      (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ K.d p q ≫ Injective.ι (K.X q))) p q hpq)
    (HomComplex.Cochain.v 0 p q hpq)

Tactic:
simp [HomComplex.δ_v 1 2 (by lia) _ p q hpq (p + 1) (p + 1) (by lia) rfl]

Premises used: CochainComplex.HomComplex.δ_v, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f (i f) n)
      (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K))).X n) (HomologicalComplex.Hom.f biprod.fst n)
        (HomComplex.Cochain.v (mappingCone.snd (𝟙 (I K))) n n ⋯)) =
    Injective.ι (K.X n)

Tactic:
simp [i]

Premises used: CochainComplex.cm5b.i
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
⊢ Mono (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f (i f) n)

Tactic:
mono_of_mono_fac (i_f_comp f n)

Premises used: CochainComplex.cm5b.i_f_comp, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ Mono (Y := mappingCone (𝟙 (I K)) ⊞ L) (i f)

Tactic:
HomologicalComplex.mono_of_mono_f (i f) inferInstance

Premises used: inferInstance, HomologicalComplex.mono_of_mono_f, CochainComplex.cm5b.i
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ CategoryStruct.comp (Y := mappingCone (𝟙 (I K)) ⊞ L) (i f) (p K L) = f

Tactic:
simp [i]

Premises used: CochainComplex.cm5b.i
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
⊢ Injective.{v_1, u_1} ((mappingCone (𝟙 (I K))).X n)

Tactic:
Injective.of_iso (HomologicalComplex.homotopyCofiber.XIsoBiprod (𝟙 (I K)) n (n + 1) rfl).symm
    inferInstance

Premises used: CategoryTheory.Injective.of_iso, CategoryTheory.CategoryStruct.id, inferInstance, CochainComplex.cm5b.I, HAdd.hAdd, CategoryTheory.Iso.symm, HomologicalComplex.homotopyCofiber.XIsoBiprod, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
rw :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ epiWithInjectiveKernel (X := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f (p K L) n)

Tactic:
rw [epiWithInjectiveKernel_iff]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩

Premises used: HomologicalComplex.Hom.f, CochainComplex.mappingCone, CategoryTheory.CategoryStruct.id, inferInstance, Nonempty.intro, CochainComplex.cm5b.I, CategoryTheory.Limits.biprod.fst, CategoryTheory.Limits.biprod.inl, Exists.intro, CategoryTheory.ShortComplex.Splitting.mk, HomologicalComplex.X, CategoryTheory.Limits.biprod.inr
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ Eq (α := (mappingCone (𝟙 (I K))).X n ⟶ L.X n)
    (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f biprod.inl n)
      (HomologicalComplex.Hom.f (p K L) n))
    0

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ ShortComplex.f
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ≫
      HomologicalComplex.Hom.f biprod.fst n =
    𝟙
      (ShortComplex.X₁
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ CategoryStruct.comp (Y :=
      ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
      (HomologicalComplex.Hom.f biprod.inr n)
      (ShortComplex.g
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯)) =
    𝟙
      (ShortComplex.X₃
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ HAdd.hAdd (α :=
      ShortComplex.X₂
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ⟶
        ShortComplex.X₂
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
      (β :=
      ShortComplex.X₂
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ⟶
        ShortComplex.X₂
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
      (CategoryStruct.comp (Y :=
        ShortComplex.X₁
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
        (HomologicalComplex.Hom.f biprod.fst n : (mappingCone (𝟙 (I K)) ⊞ L).X n ⟶ (mappingCone (𝟙 (I K))).X n)
        (ShortComplex.f
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯)))
      (ShortComplex.g
          (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
            (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ≫
        HomologicalComplex.Hom.f biprod.inr n) =
    𝟙
      (ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))

Tactic:
simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ (HomComplex.Cochain.ofHom (𝟙 (mappingCone (𝟙 (I K))))).comp
      (↑(mappingCone.fst (𝟙 (I K))) : HomComplex.Cochain (mappingCone (𝟙 (I K))) (I K) 1) ⋯ =
    HAdd.hAdd (α := HomComplex.Cochain (mappingCone (𝟙 (I K))) (I K) 1) (-HomComplex.δ 0 1 (mappingCone.snd (𝟙 (I K))))
      (HomComplex.Cochain.comp (G := mappingCone (𝟙 (I K))) (HomComplex.Cochain.ofHom 0)
        (↑(mappingCone.fst (𝟙 (I K))) : HomComplex.Cochain (mappingCone (𝟙 (I K))) (I K) 1) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ (HomComplex.Cochain.ofHom (𝟙 (mappingCone (𝟙 (I K))))).comp (mappingCone.snd (𝟙 (I K))) ⋯ =
    HAdd.hAdd (α := HomComplex.Cochain (mappingCone (𝟙 (I K))) (I K) 0) (HomComplex.δ (-1) 0 0)
        (HomComplex.Cochain.comp (mappingCone.snd (𝟙 (I K))) (HomComplex.Cochain.ofHom (𝟙 (I K))) ⋯) +
      HomComplex.Cochain.comp (G := mappingCone (𝟙 (I K))) (HomComplex.Cochain.ofHom 0) (mappingCone.snd (𝟙 (I K))) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
h₀ : Homotopy (𝟙 (mappingCone (𝟙 (I K)))) 0 :=
  mappingCone.liftHomotopy (𝟙 (I K)) (𝟙 (mappingCone (𝟙 (I K)))) 0 (mappingCone.snd (𝟙 (I K))) 0 ⋯ ⋯
h₁ : Homotopy (C := mappingCone (𝟙 (I K)) ⊞ L) (D := mappingCone (𝟙 (I K)) ⊞ L)
  (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.fst ≫ 0 ≫ biprod.inl) :=
  Homotopy.compLeft (h₀.compRight biprod.inl) biprod.fst
h₂ : Homotopy
  (HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L)
    (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.snd ≫ biprod.inr))
  (HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L) (biprod.fst ≫ 0 ≫ biprod.inl)
    (biprod.snd ≫ biprod.inr)) :=
  h₁.add (Homotopy.refl (biprod.snd ≫ biprod.inr))
⊢ p K L ≫ biprod.inr =
    HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L) (biprod.fst ≫ 0 ≫ biprod.inl)
      (biprod.snd ≫ biprod.inr)

Tactic:
simp [p]

Premises used: CochainComplex.cm5b.p
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
h₀ : Homotopy (𝟙 (mappingCone (𝟙 (I K)))) 0 :=
  mappingCone.liftHomotopy (𝟙 (I K)) (𝟙 (mappingCone (𝟙 (I K)))) 0 (mappingCone.snd (𝟙 (I K))) 0 ⋯ ⋯
h₁ : Homotopy (C := mappingCone (𝟙 (I K)) ⊞ L) (D := mappingCone (𝟙 (I K)) ⊞ L)
  (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.fst ≫ 0 ≫ biprod.inl) :=
  Homotopy.compLeft (h₀.compRight biprod.inl) biprod.fst
h₂ : Homotopy
  (HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L)
    (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.snd ≫ biprod.inr))
  (HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L) (biprod.fst ≫ 0 ≫ biprod.inl)
    (biprod.snd ≫ biprod.inr)) :=
  h₁.add (Homotopy.refl (biprod.snd ≫ biprod.inr))
⊢ HAdd.hAdd (α := mappingCone (𝟙 (I K)) ⊞ L ⟶ mappingCone (𝟙 (I K)) ⊞ L)
      (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.snd ≫ biprod.inr) =
    𝟙 (mappingCone (𝟙 (I K)) ⊞ L)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ CategoryStruct.comp (Y := mappingCone (𝟙 (I K)) ⊞ L) biprod.inr (p K L) = 𝟙 L

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ QuasiIso (K := mappingCone (𝟙 (I K)) ⊞ L) (p K L)

Tactic:
(homotopyEquiv K L).quasiIso_hom

Premises used: CochainComplex.cm5b.homotopyEquiv, HomotopyEquiv.quasiIso_hom
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).IsStrictlyGE n

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ CategoryStruct.comp (Y := mappingCone (𝟙 (cm5b.I K)) ⊞ L) (cm5b.i f) (cm5b.p K L) = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
⊢ C.d i j = 0

Tactic:
have := C.shape _ _ h
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
this : C.d i j = 0
⊢ ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x

Tactic:
rw [NatTrans.ext_iff, funext_iff] at this

Premises used: funext_iff, CategoryTheory.NatTrans.ext_iff
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
this : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
⊢ (C.d i j).app t = 0

Tactic:
this t
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
this : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
⊢ (C.d i j).app t = 0

Tactic:
exact this t
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
have := C.d_comp_d i j k
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
this : C.d i j ≫ C.d j k = 0
⊢ ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x

Tactic:
rw [NatTrans.ext_iff, funext_iff] at this

Premises used: funext_iff, CategoryTheory.NatTrans.ext_iff
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
this : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
this t
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
this : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
exact this t
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
h :
  ∀ (i : ι),
    Eq.{v_2 + 1} (α :=
      Quiver.Hom.{v_2, u_2} (V := V)
        (X.{v_2, u_2, u_3} (c := c)
          { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i)
        (X.{v_2, u_2, u_3} (c := c)
          { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i))
      (Hom.f { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := ⋯ } i)
      (Hom.f (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ })
        i)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, u_3} V c)
      { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }
      { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := ⋯ }
    (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ })

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i : ι
h : (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := V)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i))
    (Hom.f { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := ⋯ } i)
    (Hom.f (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }) i)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i : ι
h h₁ : Eq.{v_2 + 1} (α := (C.X i).obj t ⟶ (C.X i).obj t) (𝟙 ((C.X i).obj t)) (𝟙 ((C.X i).obj t))
⊢ (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)

Tactic:
rw [(C.X i).map_id]

Premises used: CategoryTheory.Functor.map_id, HomologicalComplex.X