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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
left :
  Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i)
right :
  Eq (α := (mid K L n₁).X i ⟶ L.X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
⊢ Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i) ∧
    Eq (α := (mid K L n₁).X i ⟶ L.X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)

Tactic:
constructor
-- 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₁ i : ℤ
hi : i ≠ n₁
⊢ Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i)

Tactic:
apply (isZero_single_obj_X (.up ℤ) _ _ _ hi).eq_of_tgt

Premises used: HomologicalComplex.isZero_single_obj_X, Int, CategoryTheory.Limits.IsZero.eq_of_tgt, 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
⊢ Eq (α := (mid K L n₁).X i ⟶ L.X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
inl : ∀ (hi : i < n₀), QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
inr : ∀ (hn₁ : i + 1 = n₁) (hi : i ≤ i), QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i

Tactic:
obtain (hi | rfl) := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
⊢ (ComplexShape.up ℤ).prev 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
⊢ (ComplexShape.up ℤ).next 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
inl :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i

Tactic:
rw [quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (by simp)]

Premises used: HSub.hSub, HAdd.hAdd, quasiIsoAt_iff', OfNat.ofNat
-- 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
⊢ IsIso φ.τ₁

Tactic:
have : IsIso φ.τ₁ := isIso_π_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this : IsIso φ.τ₁
⊢ IsIso φ.τ₂

Tactic:
have : IsIso φ.τ₂ := isIso_π_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this_1 : IsIso φ.τ₁
this : IsIso φ.τ₂
⊢ IsIso φ.τ₃

Tactic:
have : IsIso φ.τ₃ := isIso_π_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this_1 : IsIso φ.τ₁
this_2 : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))

Tactic:
ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Premises used: CategoryTheory.ShortComplex.quasiIso_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this_1 : IsIso φ.τ₁
this_2 : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))

Tactic:
exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Premises used: CategoryTheory.ShortComplex.quasiIso_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
inr : IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i

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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0

Tactic:
have : homologyMap (biprod.inl : _ ⟶ mid K L n₁) i = 0 :=
      (ShortComplex.isZero_homology_of_isZero_X₂ _
        (isZero_single_obj_X (.up ℤ) _ _ _ (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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
⊢ IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)

Tactic:
⟨homologyMap (σ K L n₁) i, ?_, ?_⟩

Premises used: And.intro, Exists.intro, HomologicalComplex.homologyMap, CategoryTheory.IsIso.mk, _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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
inr :
  CategoryStruct.comp (Y := homology L i) (homologyMap (π K L n₁) i) (homologyMap (σ K L n₁) i) =
    𝟙 (homology (mid K L n₁) i)
inr₁ :
  CategoryStruct.comp (Y := homology (mid K L n₁) i) (homologyMap (σ K L n₁) i) (homologyMap (π K L n₁) i) =
    𝟙 (homology L i)
⊢ IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)

Tactic:
refine ⟨homologyMap (σ K L 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
⊢ CategoryStruct.comp (Y := homology L i) (homologyMap (π K L n₁) i) (homologyMap (σ K L n₁) i) =
    𝟙 (homology (mid K L n₁) i)

Tactic:
simp [← homologyMap_id, ← biprod.total, homologyMap_comp, this]

Premises used: HomologicalComplex.homologyMap_id, CategoryTheory.Limits.biprod.total, 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
⊢ CategoryStruct.comp (Y := homology (mid K L n₁) i) (homologyMap (σ K L n₁) i) (homologyMap (π K L n₁) i) =
    𝟙 (homology L i)

Tactic:
simp [← homologyMap_comp, homologyMap_id]

Premises used: HomologicalComplex.homologyMap_id, 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i

Tactic:
have := quasiIsoAt_π K L n₀ n₁ hn₁ 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
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
rw : QuasiIsoAt f i
⊢ QuasiIsoAt (L := mid K L n₁) (ι f n₁) i

Tactic:
rw [← quasiIsoAt_iff_comp_right _ (π K L n₁), ι_π]

Premises used: quasiIsoAt_iff_comp_right, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι_π, _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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
⊢ QuasiIsoAt f i

Tactic:
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
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
⊢ QuasiIsoAt f i

Tactic:
exact 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
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
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
⊢ 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
⊢ (ComplexShape.up ℤ).next 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
rw :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X n₁),
    Eq (α := A ⟶ K.X (n₁ + 1)) (x₂ ≫ K.d n₁ (n₁ + 1)) 0 →
      ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
        x₂ ≫ Hom.f (ι f n₁) n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ →
          ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X n₀), π ≫ x₂ = x₁ ≫ K.d n₀ n₁
⊢ Mono (X := homology K n₁) (Y := homology (mid K L n₁) n₁) (homologyMap (ι f n₁) n₁)

Tactic:
rw [mono_homologyMap_iff_up_to_refinements _ n₀ n₁ (n₁ + 1) (by simp; lia) (by simp)]

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.mono_homologyMap_iff_up_to_refinements
-- 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₁
_ :
  Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0 →
    ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
      x₁ ≫ Hom.f (ι f n₁) n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
⊢ Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0 →
    ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
      x₁ ≫ Hom.f (ι f n₁) n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
_
-- 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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ Hom.f (σ K L n₁) n₀ = y₀

Tactic:
⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩

Premises used: HomologicalComplex.Hom.f, CategoryTheory.Category.comp_id, Exists.intro, CategoryTheory.CategoryStruct.comp, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π, Eq.trans
-- 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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
refine : (y₀ ≫ Hom.f (π K L n₁) n₀) ≫ Hom.f (σ K L n₁) n₀ = y₀ ≫ 𝟙 ((mid K L n₁).X n₀)
⊢ ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ Hom.f (σ K L n₁) n₀ = y₀

Tactic:
refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
-- 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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ n₀ ≠ 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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ Eq.{v_1 + 1} (α := (S K n₁).X n₀ ⟶ (S K n₁ ⊞ L).X n₀) (Hom.f biprod.inl n₀) 0

Tactic:
have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (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₀_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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
this : Eq.{v_1 + 1} (α := (S K n₁).X n₀ ⟶ (S K n₁ ⊞ L).X n₀) (Hom.f biprod.inl n₀) 0
⊢ (y₀ ≫ Hom.f (π K L n₁) n₀) ≫ Hom.f (σ K L n₁) n₀ = y₀ ≫ 𝟙 ((mid K L n₁).X n₀)

Tactic:
simp [this, ← biprod_total_f]

Premises used: HomologicalComplex.biprod_total_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₀_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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
obtain :
  ∀ (y₀ : A ⟶ L.X n₀) (hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = (y₀ ≫ Hom.f (σ K L n₁) n₀) ≫ (mid K L n₁).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 ⟨y₀, rfl⟩ : ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ (σ K L n₁).f n₀ = y₀ := by
    refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
    have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (by lia)).eq_of_src _ _
    simp [this, ← biprod_total_f]

Premises used: HomologicalComplex.Hom.f, HomologicalComplex.X, rfl, _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₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = (y₀ ≫ Hom.f (σ K L n₁) n₀) ≫ (mid K L n₁).d n₀ n₁
⊢ Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁

Tactic:
simp only [Category.assoc, Hom.comm, biprodX_ext_to_iff, biprod_lift_fst_f,
    biprod_inr_fst_f, comp_zero, biprod_lift_snd_f, biprod_inr_snd_f,
    Category.comp_id] at hy₀

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.biprod_lift_fst_f, CategoryTheory.Limits.comp_zero, HomologicalComplex.biprod_inr_snd_f, HomologicalComplex.biprod_lift_snd_f, CategoryTheory.Category.comp_id, HomologicalComplex.biprod_inr_fst_f, HomologicalComplex.biprodX_ext_to_iff, HomologicalComplex.Hom.comm
-- 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₀
hy₀ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0

Tactic:
obtain ⟨h₁, h₂⟩ := hy₀
-- 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₀
hy₀ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
⊢ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁

Tactic:
obtain ⟨h₁, h₂⟩ := hy₀
-- 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₁
rw :
  Eq (α := A ⟶ Injective.under.{v_1, u_1} (opcycles K n₁)) ((x₁ ≫ pOpcycles K n₁) ≫ Injective.ι (opcycles K n₁))
    (0 ≫ Injective.ι (opcycles K n₁))
⊢ Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0

Tactic:
rw [← cancel_mono (Injective.ι _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Injective.ι