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

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

Tactic:
rw [← IsIso.inv_hom_id_assoc ((truncGE (cokernel f) n).homologyπ n) (homologyMap (p f n) n)]

Premises used: HomologicalComplex.homologyπ, CategoryTheory.Limits.cokernel, CochainComplex.truncGE, HomologicalComplex.homologyMap, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p, CategoryTheory.IsIso.inv_hom_id_assoc
-- 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_1 : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
this_2 :
  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)
this : IsIso (X := cycles ((cokernel f).truncGE n) n) (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (inv (homologyπ ((cokernel f).truncGE n) n) ≫ homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) 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 : ℤ
inst_3 : Mono f
rw : Eq (α := homology K n ⟶ homology (cokernel f) n) (homologyMap (f ≫ cokernel.π f) n) 0
rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ homology (cokernel f) n) (homologyMap 0 n) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := homology K n ⟶ homology (cokernel f) n) 0 0
⊢ Eq (α := homology K n ⟶ homology (cokernel f) n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (cokernel.π f) n)) 0

Tactic:
rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]

Premises used: CategoryTheory.Limits.cokernel.condition, HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_zero
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
dsimp :
  Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
    (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
⊢ 𝟙 T.X₂ ≫ (homologyShortComplex f n).g = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n

Tactic:
dsimp
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
rw : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n) (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
rw₁ :
  Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n)
    (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
rw₂ rw₃ :
  Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
    (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
⊢ Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
    (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)

Tactic:
rw [Category.id_comp, ← homologyMap_comp, α]

Premises used: HomologicalComplex.homologyMap_comp, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α, CategoryTheory.Category.id_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 f
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
dsimp :
  Mono (X := T.X₃) (Y := (S f n).homology n) (homologyMap ((cokernel f).πTruncGE n ≫ p f n) n) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)
⊢ Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁

Tactic:
dsimp [φ]
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw :
  Mono (X := T.X₃) (Y := (S f n).homology n)
      (CategoryStruct.comp (Y := homology ((cokernel f).truncGE n) n) (homologyMap ((cokernel f).πTruncGE n) n)
        (homologyMap (p f n) n)) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)
⊢ Mono (X := T.X₃) (Y := (S f n).homology n) (homologyMap ((cokernel f).πTruncGE n ≫ p f n) n) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)

Tactic:
rw [homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_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 f
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono (X := T.X₃) (Y := (S f n).homology n)
      (CategoryStruct.comp (Y := homology ((cokernel f).truncGE n) n) (homologyMap ((cokernel f).πTruncGE n) n)
        (homologyMap (p f n) n)) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)

Tactic:
⟨inferInstance, inferInstance, inferInstance⟩

Premises used: inferInstance, And.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 : ℤ
inst_3 : Mono f
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono (X := T.X₃) (Y := (S f n).homology n)
      (CategoryStruct.comp (Y := homology ((cokernel f).truncGE n) n) (homologyMap ((cokernel f).πTruncGE n) n)
        (homologyMap (p f n) n)) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)

Tactic:
exact ⟨inferInstance, inferInstance, inferInstance⟩
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono φ.τ₃

Tactic:
obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩

Premises used: CategoryTheory.IsIso, CategoryTheory.Epi, CategoryTheory.Mono, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.Hom.τ₃
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
⊢ IsIso φ.τ₂

Tactic:
obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩

Premises used: CategoryTheory.IsIso, CategoryTheory.Epi, CategoryTheory.Mono, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.Hom.τ₃
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left₁ : IsIso φ.τ₂
⊢ Epi φ.τ₁

Tactic:
obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩

Premises used: CategoryTheory.IsIso, CategoryTheory.Epi, CategoryTheory.Mono, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.Hom.τ₃
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left_1 : IsIso φ.τ₂
right : Epi φ.τ₁
rw : T.Exact
⊢ (homologyShortComplex f n).Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left_1 : IsIso φ.τ₂
right : Epi φ.τ₁
⊢ T.Exact

Tactic:
(shortExact f).homology_exact₂ n

Premises used: CategoryTheory.Limits.colimit, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, CategoryTheory.Limits.colimit.ι
-- 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
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left_1 : IsIso φ.τ₂
right : Epi φ.τ₁
⊢ T.Exact

Tactic:
exact (shortExact f).homology_exact₂ n

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
rw : ∀ i < n, ExactAt (cokernel f) i
⊢ (cokernel f).IsGE n

Tactic:
rw [isGE_iff]

Premises used: CochainComplex.isGE_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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
rw : IsZero.{v_1, u_1} (homology (cokernel f) i)
⊢ ExactAt (cokernel f) i

Tactic:
rw [exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ (ComplexShape.up ℤ).Rel i (i + 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
refine_1 :
  { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f =
    0
refine_2 :
  { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.g =
    0
⊢ IsZero.{v_1, u_1} (homology (cokernel f) i)

Tactic:
refine ((shortExact f).homology_exact₃ i (i + 1) (by simp)).isZero_X₂ ?_ ?_

Premises used: CategoryTheory.ShortComplex.ShortExact.homology_exact₃, HAdd.hAdd, CategoryTheory.ShortComplex.Exact.isZero_X₂, OfNat.ofNat, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ QuasiIsoAt f i

Tactic:
have := hf i hi
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
this : QuasiIsoAt f i
refine_1 :
  Epi
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f i,
        g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f =
    0

Tactic:
rw [← ((shortExact f).homology_exact₂ i).epi_f_iff]

Premises used: CategoryTheory.ShortComplex.Exact.epi_f_iff, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
this : QuasiIsoAt f i
⊢ Epi
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f i,
        g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f

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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
refine_2 :
  Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.g =
    0

Tactic:
rw [← ((shortExact f).homology_exact₁ i (i + 1) (by simp)).mono_g_iff]

Premises used: CategoryTheory.ShortComplex.Exact.mono_g_iff, HAdd.hAdd, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, OfNat.ofNat, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.shortExact