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
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
pos :
  ∀ (hi' : i + 1 < n),
    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
neg :
  ∀ (hi' : ¬i + 1 < n),
    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
⊢ 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

Tactic:
by_cases hi' : i + 1 < 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
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
hi' : i + 1 < 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
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
hi' : i + 1 < n
⊢ QuasiIsoAt f (i + 1)

Tactic:
have := hf (i + 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
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
hi' : i + 1 < n
this : QuasiIsoAt f (i + 1)
⊢ 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

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
hi' : ¬i + 1 < n
⊢ n = 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
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
hi' : ¬i + 1 < n
⊢ ∀ i_1 < i + 1, QuasiIsoAt f i_1

Tactic:
obtain rfl : n = i + 1 := by lia

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
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
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
⊢ Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))

Tactic:
obtain rfl : n = i + 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : 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_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
inst : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
⊢ i < i + 1

Tactic:
obtain rfl : n = i + 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : 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_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
inst : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
hi₁ : i < i + 1
⊢ ¬i + 1 < i + 1

Tactic:
obtain rfl : n = i + 1 := by lia

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 : Mono f
i : ℤ
hf : ∀ i_1 < i + 1, QuasiIsoAt f i_1
inst_3 : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
hi : i < i + 1
hi' : ¬i + 1 < i + 1
⊢ 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

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)
rw : (cokernel f).IsGE n
⊢ QuasiIso (L := (cokernel f).truncGE n) ((cokernel f).πTruncGE n)

Tactic:
rw [quasiIso_πTruncGE_iff]

Premises used: CochainComplex.quasiIso_πTruncGE_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)
⊢ (cokernel f).IsGE n

Tactic:
isGE_cokernel f n hf

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.isGE_cokernel
-- 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)
⊢ (cokernel f).IsGE n

Tactic:
exact isGE_cokernel f n hf

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.isGE_cokernel
-- 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq : q ≤ n
inl : ∀ (hq : q < n), QuasiIsoAt (L := mid f n) (ι f n) q
inr : ∀ (hq : n ≤ n), QuasiIsoAt (L := mid f n) (ι f n) n
⊢ QuasiIsoAt (L := mid f n) (ι f n) q

Tactic:
obtain hq | rfl := hq.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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq_1 : q ≤ n
hq : q < n
⊢ QuasiIsoAt (K := mid f n) (π f n) q

Tactic:
have := quasiIsoAt_π 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq_1 : q ≤ n
hq : q < n
this : QuasiIsoAt (K := mid f n) (π f n) q
inl : QuasiIsoAt f q
⊢ QuasiIsoAt (L := mid f n) (ι f n) q

Tactic:
rw [← quasiIsoAt_iff_comp_right _ (π f n), mappingCocone.lift_fst]

Premises used: quasiIsoAt_iff_comp_right, CochainComplex.mappingCocone.lift_fst, _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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq_1 : q ≤ n
hq : q < n
this : QuasiIsoAt (K := mid f n) (π f n) q
⊢ QuasiIsoAt f q

Tactic:
hf 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq_1 : q ≤ n
hq : q < n
this : QuasiIsoAt (K := mid f n) (π f n) q
⊢ QuasiIsoAt f q

Tactic:
exact hf 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
⊢ Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)

Tactic:
have := mono_homologyMap_π f n n (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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
dsimp :
  Mono (X := homology (mappingCocone (L := S f n) (α f n)) n) (Y := homology L n)
    (homologyMap (mappingCocone.fst (α f n)) n)
⊢ Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
⊢ Mono (X := homology (mappingCocone (L := S f n) (α f n)) n) (Y := homology L n)
    (homologyMap (mappingCocone.fst (α 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
⊢ Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)

Tactic:
have : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n) :=
      by dsimp; 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
inr : ∀ (h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)), QuasiIsoAt (L := mid f n) (ι f n) n
⊢ QuasiIsoAt (L := mid f n) (ι f n) n

Tactic:
have h₁ := (exact_homologyShortComplex f n).fIsKernel
-- 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
inr :
  ∀
    (h₂ :
      IsLimit
        (KernelFork.ofι
          { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n,
              X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
              X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
              f := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n,
              g := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₂ n, zero := ⋯ :
              ShortComplex.{v_1, u_1} C }.f
          ⋯)),
    QuasiIsoAt (L := mid f n) (ι f n) n
⊢ QuasiIsoAt (L := mid f n) (ι f n) n

Tactic:
have h₂ := (CochainComplex.homologyMap_exact₂_of_distTriang _
      (DerivedCategory.mappingCocone_triangle_distinguished (α f n)) n).fIsKernel
-- 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₂ n, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.f
      ⋯)
⊢ homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom

Tactic:
simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]

Premises used: CochainComplex.mappingCocone.lift_fst, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.cancel_mono, HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π, CategoryTheory.Limits.WalkingParallelPair.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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₂ n, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.f
      ⋯)
⊢ homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom

Tactic:
have : homologyMap (ι f n) n = (IsLimit.conePointUniqueUpToIso h₁ h₂).hom := by
      simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]
-- 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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this_2 :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₂ n, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.f
      ⋯)
this : homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom
inr : IsIso (h₁.conePointUniqueUpToIso h₂).hom
⊢ QuasiIsoAt (L := mid f n) (ι f n) n

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap, this]

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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this_1 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
this_2 :
  Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₂ n, zero := ⋯ :
          ShortComplex.{v_1, u_1} C }.f
      ⋯)
this : homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom
⊢ IsIso (h₁.conePointUniqueUpToIso h₂).hom

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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
inst_4 : Mono (X := homology K n₁) (Y := homology L n₁) (homologyMap f n₁)
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₁
j : ℤ
hj : j < n₁
⊢ j ≤ 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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
obtain :
  ∀ (F₁ : (cofFib f).FullSubcategory) (h₁ : quasiIsoLE n₀ F₁) (h₂ : isIsoLE n₀ F₁),
    Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁) →
      ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F
⊢ ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F

Tactic:
obtain ⟨F₁, h₁, h₂, _⟩ := step₁ f n₀ n₁ hf

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁