awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
h : QuasiIso i
⊢ HomologicalComplex.Acyclic (cokernel i)
have this₁ : (ShortComplex.mk (X₃ := cokernel i) i (cokernel.π i) sorry).ShortExact
Tactic: have : (ShortComplex.mk _ _ (cokernel.condition i)).ShortExact :=
          { exact := ShortComplex.exact_cokernel i }
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
h : QuasiIso p
⊢ ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
have inr : HomologicalComplex.Acyclic (kernel p)
Tactic: refine IsKInjective.eq_δ_of_cocycle' β ?_ 0 (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
h : QuasiIso p
⊢ HomologicalComplex.Acyclic (kernel p)
have this₁ : Epi p
Tactic: have := hp.epi
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this_3 : (kernel p).IsKInjective
h : QuasiIso p
this : Epi p
⊢ HomologicalComplex.Acyclic (kernel p)
have this₁ : (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p sorry).ShortExact
Tactic: have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ ∀ {Y : Plus.{u_2, u_1} C} (f : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯ ⟶ Y),
    Nonempty
      (MorphismProperty.MapFactorizationData (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C))
        f)
have 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 sorry)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
  Nonempty
    (MorphismProperty.MapFactorizationData (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C)) f)
Tactic: ⟨L, m, hm⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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 :
      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 (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C))
        f)
have this : ∀
  (f :
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) ⟶
      ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
  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 sorry) (Y :=
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
      { 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 sorry)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
Tactic: ⟨f⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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 ⋯)
⊢ 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 ⋯) })
have 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 sorry)
          (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
          { 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 sorry)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
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)⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ 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 ⋯) })
have 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 sorry) ⟶
          K')
      (p :
        K' ⟶
          ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
      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 sorry) (Y :=
                ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
                { 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 sorry)
                    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
Tactic: obtain ⟨K', _, i, p, _, _, hp, fac⟩ := cm5a f d
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ 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)
have rwa : Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) (Y :=
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry)
  (ObjectProperty.homMk (P := CochainComplex.plus C) i)
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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)
⊢ 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)
have rwa₁ : Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) (Y :=
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry)
  (ObjectProperty.homMk (P := CochainComplex.plus C) i)
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]