awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
obtain :
  ∀ (d : ℤ),
    K.IsStrictlyGE (d + 1) →
      L.IsStrictlyGE d →
        Nonempty
          (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (trivialCofibrations (Plus.{u_2, u_1} C))
            (fibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
            (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
            { hom := f :
              InducedCategory.Hom (C :=
                ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
                CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
                (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
                (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (trivialCofibrations (Plus.{u_2, u_1} C))
      (fibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
obtain :
  ∀ (K' : CochainComplex.{u_2, u_1, 0} C ℤ),
    K'.IsStrictlyGE d →
      ∀
        (i :
          ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
            K')
        (p :
          K' ⟶
            ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
        Mono i →
          QuasiIso i →
            ∀ (hp : degreewiseEpiWithInjectiveKernel p) (fac : i ≫ p = f),
              Nonempty
                (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C)
                  (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C)) (X :=
                  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
                  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
                  { hom := f :
                    InducedCategory.Hom (C :=
                      ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C))
                      (D := CochainComplex.{u_2, u_1, 0} C ℤ) (F :=
                      ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
                      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
                      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (trivialCofibrations (Plus.{u_2, u_1} C))
      (fibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
obtain ⟨K', _, i, p, _, _, hp, fac⟩ := cm5a f d

Premises used: CochainComplex.Plus.modelCategoryQuillen.cm5a
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
left_1 : Mono i
left_2 : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
rwa :
  Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₁ :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₂ rwa₃ rwa₄ rwa₅ :
  Mono (C := CochainComplex.{u_2, u_1, 0} C ℤ) (X :=
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯))
    (Y :=
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯))
    (InducedCategory.Hom.hom (ObjectProperty.homMk (P := CochainComplex.plus C) i))
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)

Tactic:
rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]

Premises used: CochainComplex.Plus.mono_iff, CochainComplex.Plus.modelCategoryQuillen.cofibration_iff, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
left_1 : Mono i
left_2 : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ weakEquivalences (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
left_1 : Mono i
left_2 : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (trivialCofibrations (Plus.{u_2, u_1} C))
      (fibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
exact ⟨{
      Z := ⟨K', d, inferInstance⟩
      i := ObjectProperty.homMk i
      p := ObjectProperty.homMk p
      hi :=
        ⟨by rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff],
          by assumption⟩
      hp := hp }⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
this :
  ∀ (L : CochainComplex.{u_2, u_1, 0} C ℤ) (m : ℤ) (hm : L.IsStrictlyGE m)
    (f :
      Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C))
        f)
⊢ ∀ {Y : Plus.{u_2, u_1} C} (f : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯ ⟶ Y),
    Nonempty
      (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C))
        f)

Tactic:
⟨L, m, hm⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
this :
  ∀
    (f :
      ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
        ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
        (trivialFibrations (Plus.{u_2, u_1} C)) (X :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
        { hom := f :
          InducedCategory.Hom (C :=
            ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
            CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ ∀
    (f :
      Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C))
        f)

Tactic:
⟨f⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
obtain :
  ∀ (d : ℤ),
    K.IsStrictlyGE (d + 1) →
      L.IsStrictlyGE d →
        Nonempty
          (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
            (trivialFibrations (Plus.{u_2, u_1} C)) (X :=
            ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
            ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
            { hom := f :
              InducedCategory.Hom (C :=
                ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
                CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
                (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
                (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
      (trivialFibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
obtain :
  ∀ (K' : CochainComplex.{u_2, u_1, 0} C ℤ),
    K'.IsStrictlyGE d →
      ∀
        (i :
          ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
            K')
        (p :
          K' ⟶
            ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
        Mono i →
          ∀ (hp : degreewiseEpiWithInjectiveKernel p),
            QuasiIso p →
              ∀ (fac : i ≫ p = f),
                Nonempty
                  (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
                    (trivialFibrations (Plus.{u_2, u_1} C)) (X :=
                    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
                    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
                    { hom := f :
                      InducedCategory.Hom (C :=
                        ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C))
                        (D := CochainComplex.{u_2, u_1, 0} C ℤ) (F :=
                        ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
                        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
                        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
      (trivialFibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
obtain ⟨K', _, i, p, _, hp, _, fac⟩ := cm5b f d

Premises used: CochainComplex.cm5b
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
w_1 : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w_2 : QuasiIso p
fac : i ≫ p = f
rwa :
  Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₁ :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₂ rwa₃ rwa₄ rwa₅ :
  Mono (C := CochainComplex.{u_2, u_1, 0} C ℤ) (X :=
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯))
    (Y :=
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯))
    (InducedCategory.Hom.hom (ObjectProperty.homMk (P := CochainComplex.plus C) i))
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)

Tactic:
rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]

Premises used: CochainComplex.Plus.mono_iff, CochainComplex.Plus.modelCategoryQuillen.cofibration_iff, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
w_1 : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w_2 : QuasiIso p
fac : i ≫ p = f
⊢ weakEquivalences (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)

Tactic:
assumption