awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ ∃ (q : ℕ), IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)

Tactic:
⟨(i - n₀).natAbs, isIso_midπ_f f n₀ _ i⟩

Premises used: HSub.hSub, Int.natAbs, Exists.intro, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIso_midπ_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
obtain : ∀ (q : ℕ), IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i) → Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)
⊢ Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)

Tactic:
obtain ⟨q, _⟩ : ∃ (q : ℕ), IsIso ((midπ f n₀ q).f i) :=
      ⟨(i - n₀).natAbs, isIso_midπ_f f n₀ _ i⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
h : IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)
⊢ Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)

Tactic:
mono_of_mono_fac (ι_midπ_f f n₀ q i)

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ_f, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
h : IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)
⊢ Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)

Tactic:
exact mono_of_mono_fac (ι_midπ_f f n₀ q i)

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ_f, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ i + 1 ≤ n₀ + (↑(i + 1 - n₀).natAbs : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
obtain : ∀ (q : ℕ) (hq : i + 1 ≤ n₀ + (↑q : ℤ)), QuasiIsoAt (L := mid f n₀) (ι f n₀) i
⊢ QuasiIsoAt (L := mid f n₀) (ι f n₀) i

Tactic:
obtain ⟨q, hq⟩ : ∃ (q : ℕ), i + 1 ≤ n₀ + q := ⟨(i + 1 - n₀).natAbs, by lia⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
⊢ QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i

Tactic:
have := quasiIsoAt_midπ f n₀ q i hq
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
this : QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i
rw : QuasiIsoAt ((functor f n₀).obj (op q)).obj (P := cofFib f).ι i
⊢ QuasiIsoAt (L := mid f n₀) (ι f n₀) i

Tactic:
rw [← quasiIsoAt_iff_comp_right _ (midπ f n₀ q), ι_midπ]

Premises used: quasiIsoAt_iff_comp_right, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
this : QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i
⊢ i ≤ n₀ + (↑q : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
this : QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i
⊢ QuasiIsoAt ((functor f n₀).obj (op q)).obj (P := cofFib f).ι i

Tactic:
exact (CofFibFactorizationQuasiIsoLE.sequence f n₀ q).property i (by lia)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ i ≤ n₀ + (↑(i - n₀).natAbs : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
obtain : ∀ (q : ℕ) (hq : i ≤ n₀ + (↑q : ℤ)), epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)
⊢ epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)

Tactic:
obtain ⟨q, hq⟩ : ∃ (q : ℕ), i ≤ n₀ + q := ⟨(i - n₀).natAbs, by lia⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
rw : epiWithInjectiveKernel (Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i)
⊢ epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)

Tactic:
rw [← midπ_π_f f n₀ q]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π_f
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
⊢ IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)

Tactic:
have := isIso_midπ_f f n₀ q i
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
this : IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)
⊢ epiWithInjectiveKernel (Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i)

Tactic:
MorphismProperty.comp_mem _ _ _
    (epiWithInjectiveKernel_of_iso _)
    ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj.property.2 i)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.MorphismProperty.comp_mem, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence, And.right, CategoryTheory.Abelian.epiWithInjectiveKernel_of_iso
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
this : IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)
⊢ epiWithInjectiveKernel (Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i)

Tactic:
exact MorphismProperty.comp_mem _ _ _
    (epiWithInjectiveKernel_of_iso _)
    ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj.property.2 i)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.MorphismProperty.comp_mem, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence, And.right, CategoryTheory.Abelian.epiWithInjectiveKernel_of_iso
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : L.IsStrictlyGE n
inst_5 : Mono f
⊢ n = n - 1 + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : L.IsStrictlyGE n
inst_5 : Mono f
obtain :
  ∀ (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE (n + 1)],
    ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE (n + 1)) (ι : K ⟶ K') (π : K' ⟶ L),
      Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f

Tactic:
obtain ⟨n, rfl⟩ : ∃ (q : ℤ), n = q + 1 := ⟨n - 1, by simp⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE (n + 1)) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f

Tactic:
⟨mid f n, inferInstance, ι f n, π f n, inferInstance,
    inferInstance, degreewiseEpiWithInjectiveKernel_π f n, ι_π f n⟩

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π, inferInstance, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_π, And.intro, Exists.intro, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.degreewiseEpiWithInjectiveKernel_π, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE (n + 1)) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f

Tactic:
exact ⟨mid f n, inferInstance, ι f n, π f n, inferInstance,
    inferInstance, degreewiseEpiWithInjectiveKernel_π f n, ι_π f n⟩
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ K.IsStrictlyGE n

Tactic:
have : K.IsStrictlyGE n := K.isStrictlyGE_of_ge n (n + 1) (by lia)
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
obtain :
  ∀ (L' : CochainComplex.{v_1, u_1, 0} C ℤ),
    L'.IsStrictlyGE n →
      ∀ (i : K ⟶ L') (p : L' ⟶ L),
        Mono i →
          ∀ (hp : degreewiseEpiWithInjectiveKernel p),
            QuasiIso p →
              ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
                Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = i ≫ p
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f

Tactic:
obtain ⟨L', _, i, p, _, hp, _, rfl⟩ := cm5b f n

Premises used: rfl, CochainComplex.cm5b
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex.{v_1, u_1, 0} C ℤ
w : L'.IsStrictlyGE n
i : K ⟶ L'
p : L' ⟶ L
w_1 : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w_2 : QuasiIso p
obtain :
  ∀ (K' : CochainComplex.{v_1, u_1, 0} C ℤ),
    K'.IsStrictlyGE n →
      ∀ (ι : K ⟶ K') (π : K' ⟶ L'),
        Mono ι →
          QuasiIso ι →
            ∀ (hπ : degreewiseEpiWithInjectiveKernel π),
              Mono (ι ≫ π) →
                ∃ (K'_1 : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'_1.IsStrictlyGE n) (ι_1 : K ⟶ K'_1) (π_1 : K'_1 ⟶ L),
                  Mono ι_1 ∧ QuasiIso ι_1 ∧ degreewiseEpiWithInjectiveKernel π_1 ∧ ι_1 ≫ π_1 = (ι ≫ π) ≫ p
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = i ≫ p

Tactic:
obtain ⟨K', _, ι, π, _, _, hπ, rfl⟩ := cm5a_cof i n

Premises used: CochainComplex.Plus.modelCategoryQuillen.cm5a_cof, rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex.{v_1, u_1, 0} C ℤ
w : L'.IsStrictlyGE n
p : L' ⟶ L
hp : degreewiseEpiWithInjectiveKernel p
w_1 : QuasiIso p
K' : CochainComplex.{v_1, u_1, 0} C ℤ
w_2 : K'.IsStrictlyGE n
ι : K ⟶ K'
π : K' ⟶ L'
left : Mono ι
left_1 : QuasiIso ι
hπ : degreewiseEpiWithInjectiveKernel π
w_3 : Mono (ι ≫ π)
⊢ ι ≫ π ≫ p = (ι ≫ π) ≫ p

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex.{v_1, u_1, 0} C ℤ
w : L'.IsStrictlyGE n
p : L' ⟶ L
hp : degreewiseEpiWithInjectiveKernel p
w_1 : QuasiIso p
K' : CochainComplex.{v_1, u_1, 0} C ℤ
w_2 : K'.IsStrictlyGE n
ι : K ⟶ K'
π : K' ⟶ L'
left : Mono ι
left_1 : QuasiIso ι
hπ : degreewiseEpiWithInjectiveKernel π
w_3 : Mono (ι ≫ π)
⊢ ∃ (K'_1 : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'_1.IsStrictlyGE n) (ι_1 : K ⟶ K'_1) (π_1 : K'_1 ⟶ L),
    Mono ι_1 ∧ QuasiIso ι_1 ∧ degreewiseEpiWithInjectiveKernel π_1 ∧ ι_1 ≫ π_1 = (ι ≫ π) ≫ p

Tactic:
exact ⟨K', inferInstance, ι, π ≫ p, inferInstance, inferInstance,
    MorphismProperty.comp_mem _ _ _ hπ hp, by 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
n : ℤ
dsimp : Injective.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X n))
⊢ Injective.{v_1, u_1} ((I K).X n)

Tactic:
dsimp
-- 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} (Injective.under.{v_1, u_1} (K.X 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
rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((I K).X i)
⊢ (I K).IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_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 ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((I K).X i)

Tactic:
Injective.isZero_under _ (K.isZero_of_isStrictlyGE n i hi)

Premises used: CategoryTheory.Injective.isZero_under, CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Injective.under
-- 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
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((I K).X i)

Tactic:
exact Injective.isZero_under _ (K.isZero_of_isStrictlyGE n i hi)

Premises used: CategoryTheory.Injective.isZero_under, CochainComplex.isZero_of_isStrictlyGE
-- 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
rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mappingCone (𝟙 (I K)) ⊞ L).X i)
⊢ (mappingCone (𝟙 (I K)) ⊞ L).IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_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 ℤ
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} ((mappingCone (𝟙 (I K)) ⊞ L).X i)

Tactic:
IsZero.of_iso ?_ ((HomologicalComplex.eval C (ComplexShape.up ℤ) i).mapBiprod _ _)

Premises used: HomologicalComplex.eval, Int, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Functor.mapBiprod, ComplexShape.up
-- 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
refine :
  IsZero.{v_1, u_1}
    (biprod.{v_1, u_1} (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) (mappingCone (𝟙 (I K))))
      (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) L))
⊢ IsZero.{v_1, u_1} ((mappingCone (𝟙 (I K)) ⊞ L).X i)

Tactic:
refine IsZero.of_iso ?_ ((HomologicalComplex.eval C (ComplexShape.up ℤ) i).mapBiprod _ _)

Premises used: HomologicalComplex.eval, Int, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Functor.mapBiprod, ComplexShape.up
-- 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
simp :
  (IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1))) ∧
      IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
    IsZero.{v_1, u_1} (L.X i)
⊢ IsZero.{v_1, u_1}
    (biprod.{v_1, u_1} (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) (mappingCone (𝟙 (I K))))
      (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) L))

Tactic:
simp only [HomologicalComplex.eval_obj, biprod_isZero_iff, mappingCone.isZero_X_iff, I_X]

Premises used: HomologicalComplex.eval_obj, CochainComplex.mappingCone.isZero_X_iff, CategoryTheory.Limits.biprod_isZero_iff, CochainComplex.cm5b.I_X
-- 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 + 1))) ∧
      IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
    IsZero.{v_1, u_1} (L.X i)

Tactic:
⟨⟨?_, ?_⟩, L.isZero_of_isStrictlyGE n i hi⟩

Premises used: CochainComplex.isZero_of_isStrictlyGE, And.intro
-- 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
refine_1 : IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1)))
refine_2 : IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))
⊢ (IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1))) ∧
      IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
    IsZero.{v_1, u_1} (L.X i)

Tactic:
refine ⟨⟨?_, ?_⟩, L.isZero_of_isStrictlyGE n i hi⟩
-- 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 + 1)))

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 + 1)))

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

Premises used: CochainComplex.cm5b.I, CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, OfNat.ofNat