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
n₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ Eq (α := A ⟶ Injective.under.{v_1, u_1} (opcycles K n₁)) ((x₁ ≫ pOpcycles K n₁) ≫ Injective.ι (opcycles K n₁))
    (0 ≫ Injective.ι (opcycles K n₁))

Tactic:
simpa [i, ← cancel_mono (singleObjXSelf (.up ℤ) n₁ _).hom] using h₁

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.i, Int, CategoryTheory.cancel_mono, HomologicalComplex.singleObjXSelf, CategoryTheory.Iso.hom, ComplexShape.up
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0

Tactic:
replace h₁ : x₁ ≫ K.pOpcycles n₁ = 0 := by
    rw [← cancel_mono (Injective.ι _)]
    simpa [i, ← cancel_mono (singleObjXSelf (.up ℤ) n₁ _).hom] using h₁
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
simp : n₁ - 1 = n₀
⊢ (ComplexShape.up ℤ).prev n₁ = n₀

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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
⊢ n₁ - 1 = n₀

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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
obtain :
  ∀ (A₁ : C) (π : A₁ ⟶ A),
    Epi π →
      ∀ (x₀ : A₁ ⟶ K.X n₀) (hx₀ : π ≫ x₁ = x₀ ≫ K.d n₀ n₁),
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
obtain ⟨A₁, π, _, x₀, hx₀⟩ :=
    (K.comp_pOpcycles_eq_zero_iff_up_to_refinements x₁ n₀ (by simp; lia)).1 h₁

Premises used: HomologicalComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements, Iff.mp, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
A₁ : C
π : A₁ ⟶ A
w : Epi π
x₀ : A₁ ⟶ K.X n₀
hx₀ : π ≫ x₁ = x₀ ≫ K.d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
⟨A₁, π, inferInstance, x₀, hx₀⟩

Premises used: inferInstance, Exists.intro
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
A₁ : C
π : A₁ ⟶ A
w : Epi π
x₀ : A₁ ⟶ K.X n₀
hx₀ : π ≫ x₁ = x₀ ≫ K.d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
exact ⟨A₁, π, inferInstance, x₀, hx₀⟩
-- 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₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ i ≠ n₁

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 i : ℤ
hi : i + 1 = n
⊢ Eq (α := ((cokernel f).truncGE n).X i ⟶ Injective.under.{v_1, u_1} (((cokernel f).truncGE n).X n))
    (((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n)) 0

Tactic:
(isZero_of_isStrictlyGE _ n _).eq_of_src _ _

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src
-- 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 i : ℤ
hi : i + 1 = n
⊢ Eq (α := ((cokernel f).truncGE n).X i ⟶ Injective.under.{v_1, u_1} (((cokernel f).truncGE n).X n))
    (((cokernel f).truncGE n).d i n ≫ Injective.ι (((cokernel f).truncGE n).X n)) 0

Tactic:
exact (isZero_of_isStrictlyGE _ n _).eq_of_src _ _

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src
-- 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 : ℤ
simp :
  Mono.{v_1, u_1} (Y := Injective.under.{v_1, u_1} (((cokernel f).truncGE n).X n))
    (Injective.ι (((cokernel f).truncGE n).X n))
⊢ Mono (Y := (S f n).X n) (Hom.f (p f n) n)

Tactic:
simp only [p, mkHomToSingle_f, mono_comp_iff_of_mono]

Premises used: HomologicalComplex.mkHomToSingle_f, CategoryTheory.mono_comp_iff_of_mono, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p
-- 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 : ℤ
⊢ Mono.{v_1, u_1} (Y := Injective.under.{v_1, u_1} (((cokernel f).truncGE n).X n))
    (Injective.ι (((cokernel f).truncGE n).X n))

Tactic:
infer_instance
-- 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 : ℤ
⊢ Eq (α := K ⟶ S f n) (f ≫ α f n) 0

Tactic:
simp [α]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α
-- 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 i : ℤ
⊢ Eq (α := K.X i ⟶ (S f n).X i) (f.f i ≫ Hom.f (α f n) i) 0

Tactic:
simp [← comp_f]

Premises used: HomologicalComplex.comp_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
n : ℤ
⊢ HAdd.hAdd (α := Cochain K (S f n) 0) (δ (-1) 0 0) (Cochain.ofHom (f ≫ α f n)) = 0

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 : ℤ
⊢ CategoryStruct.comp (Y := mid f n) (ι f n) (π f n) = f

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 : Mono f
⊢ Mono (Y := mid f n) (ι f n)

Tactic:
mono_of_mono_fac (ι_π f n)

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι_π, 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
n i : ℤ
rw :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ (mid f n).X i) (w : f_1 ≫ Hom.f (π f n) i = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mid f n).X i, X₃ := L.X i, f := f_1, g := Hom.f (π f n) i, zero := w :
          ShortComplex.{v_1, u_1} C }.Splitting
⊢ epiWithInjectiveKernel (X := (mid f n).X i) (Hom.f (π f n) i)

Tactic:
rw [epiWithInjectiveKernel_iff]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
-- 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 i : ℤ
⊢ i - 1 + 1 = i

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 i : ℤ
⊢ Eq (α := (S f n).X (i - 1) ⟶ L.X i)
    (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯ ≫ Hom.f (π f n) i)
    0

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 i : ℤ
⊢ i + -1 = i - 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 i : ℤ
⊢ i + 0 = i

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 i : ℤ
⊢ HAdd.hAdd (α :=
      (ShortComplex.mk (X₁ := (S f n).X (i - 1))
            (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
            (Hom.f (π f n) i) ⋯).X₂ ⟶
        (ShortComplex.mk (X₁ := (S f n).X (i - 1))
            (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
            (Hom.f (π f n) i) ⋯).X₂)
      (β :=
      (ShortComplex.mk (X₁ := (S f n).X (i - 1))
            (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
            (Hom.f (π f n) i) ⋯).X₂ ⟶
        (ShortComplex.mk (X₁ := (S f n).X (i - 1))
            (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
            (Hom.f (π f n) i) ⋯).X₂)
      ((ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).g ≫
          Cochain.v (mappingCocone.inl (α f n)) i i ⋯ :
        (ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).X₂ ⟶
          (ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).X₂)
      (Cochain.v (mappingCocone.snd (α f n)) i (i - 1) ⋯ ≫
          (ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).f :
        (ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).X₂ ⟶
          (ShortComplex.mk (X₁ := (S f n).X (i - 1))
              (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
              (Hom.f (π f n) i) ⋯).X₂) =
    𝟙
      (ShortComplex.mk (X₁ := (S f n).X (i - 1))
          (Cochain.v (↑(mappingCocone.inr (α f n)) : Cochain (S f n) (mappingCocone (α f n)) 1) (i - 1) i ⋯)
          (Hom.f (π f n) i) ⋯).X₂

Tactic:
simp [mappingCocone.id_X]

Premises used: CochainComplex.mappingCocone.id_X
-- 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 i : ℤ
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ (mid f n).X i) (w : f_1 ≫ Hom.f (π f n) i = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mid f n).X i, X₃ := L.X i, f := f_1, g := Hom.f (π f n) i, zero := w :
          ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
exact ⟨_, inferInstance, (mappingCocone.inr (α f n)).1.v (i - 1) i (by lia), by simp,
    ⟨{r := (mappingCocone.snd (α f n)).v _ _ (by lia)
      s := (mappingCocone.inl (α f n)).v _ _ (by lia)
      id := (add_comm _ _).trans (by simp [mappingCocone.id_X]) }⟩⟩
-- 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 i : ℤ
hi : i ≤ n
⊢ CategoryStruct.comp (Y := (mid f n).X i) (Cochain.v (mappingCocone.inl (α f n)) i i ⋯) (Hom.f (π f n) i) = 𝟙 (L.X i)

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 i : ℤ
hi : i ≤ n
refine : Hom.f (π f n) i ≫ Cochain.v (mappingCocone.inl (α f n)) i i ⋯ = 𝟙 ((mid f n).X i)
⊢ IsIso (X := (mid f n).X i) (Hom.f (π f n) i)

Tactic:
refine ⟨(mappingCocone.inl (α f n)).v i i (add_zero i), ?_, by 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 i : ℤ
hi : i ≤ n
⊢ i + -1 = i - 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 i : ℤ
hi : i ≤ n
⊢ i - 1 ≠ n

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 i : ℤ
hi : i ≤ n
⊢ i - 1 + 1 = i

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 i : ℤ
hi : i ≤ n
⊢ Hom.f (π f n) i ≫ Cochain.v (mappingCocone.inl (α f n)) i i ⋯ = 𝟙 ((mid f n).X i)

Tactic:
simp [← mappingCocone.id_X (α f n) i (i - 1) (by lia),
    (isZero_single_obj_X _ _ _ _ (by lia)).eq_of_src
      ((mappingCocone.inr (α f n)).1.v (i - 1) i (by lia)) 0]

Premises used: HomologicalComplex.isZero_single_obj_X, HSub.hSub, CochainComplex.mappingCocone.inr, CochainComplex.mappingCocone.id_X, CategoryTheory.Limits.IsZero.eq_of_src, CochainComplex.HomComplex.Cochain.v, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α, OfNat.ofNat, Subtype.val
-- 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 q : ℤ
hq : q ≤ n
⊢ q - 1 + 1 = 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
n q : ℤ
hq : q ≤ n
⊢ q - 1 ≠ n

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 q : ℤ
hq : q < n
⊢ q ≠ n

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 q : ℤ
hq : q < n
⊢ q ≤ n

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 q : ℤ
hq : q < n
⊢ Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)

Tactic:
have := mono_homologyMap_π f n q (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 q : ℤ
hq : q < n
this : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
⊢ Epi (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)

Tactic:
have := epi_homologyMap_π f n q 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
n q : ℤ
hq : q < n
this_1 : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
this : Epi (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
rw : IsIso (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
⊢ QuasiIsoAt (K := mid f n) (π f n) q

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- 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 q : ℤ
hq : q < n
this_1 : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
this : Epi (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
⊢ IsIso (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)

Tactic:
apply Balanced.isIso_of_mono_of_epi

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- 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 : ℤ
rw : Eq (α := homology K n ⟶ (S f n).homology n) (homologyMap (f ≫ α f n) n) 0
rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ (S f n).homology n) (homologyMap 0 n) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := homology K n ⟶ (S f n).homology n) 0 0
⊢ Eq (α := homology K n ⟶ (S f n).homology n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (α f n) n)) 0

Tactic:
rw [← homologyMap_comp, comp_α, homologyMap_zero]

Premises used: HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_zero, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.comp_α
-- 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 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
⊢ Mono (homologyShortComplex f n).f

Tactic:
assumption
-- 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 : ℤ
⊢ (ComplexShape.up ℤ).prev n = n - 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 : ℤ
⊢ Eq (α := (S f n).X (n - 1) ⟶ (S f n).X n) ((S f n).d (n - 1) n) 0

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 : ℤ
⊢ IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)

Tactic:
have := (S f n).isIso_homologyπ (n - 1) n (by simp) (by 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 : ℤ
this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
rw : Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (cyclesMap (p f n) n ≫ (S f n).homologyπ n)
⊢ Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)

Tactic:
rw [homologyπ_naturality (p f n) n]

Premises used: HomologicalComplex.homologyπ_naturality, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p
-- 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 : ℤ
this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
⊢ Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (cyclesMap (p f n) n ≫ (S f n).homologyπ n)

Tactic:
infer_instance
-- 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 : ℤ
this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
⊢ Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)

Tactic:
have : Mono ((truncGE (cokernel f) n).homologyπ n ≫ homologyMap (p f n) n) := by
    rw [homologyπ_naturality (p f n) n]
    infer_instance