awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
obtain :
  ∀ (F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory) (h₃ : quasiIsoLE n₁ F₂) (h₄ : isIsoLE n₁ F₂),
    ∃ (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₁.obj.ι n₀ n₁ h₁

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂, CategoryTheory.Factorisation.ι
-- 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₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
dsimp : Mono F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι
⊢ Mono (Y :=
    Factorisation.mid (f := f)
      { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid, ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
        π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ })
    (Factorisation.ι
      { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid, ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
        π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ })

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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
⊢ Mono F₂.obj (P := cofFib F₁.obj (P := cofFib 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
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
refine :
  ∀ (i : ℤ) (hi : i ≤ n₀),
    IsIso (X :=
      (Factorisation.mid (f := f)
            (ObjectProperty.FullSubcategory.obj (P := cofFib f)
              (ObjectProperty.FullSubcategory.mk (P := cofFib f)
                { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid,
                  ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
                  π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ :
                  Factorisation f }
                ⋯))).X
        i)
      (Hom.f
        (Factorisation.π
          (ObjectProperty.FullSubcategory.obj (P := cofFib f)
            (ObjectProperty.FullSubcategory.mk (P := cofFib f)
              { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid,
                ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
                π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ }
              ⋯)))
        i)
⊢ ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F

Tactic:
refine ⟨.mk { mid := F₂.obj.mid, ι := F₂.obj.ι, π := F₂.obj.π ≫ F₁.obj.π }
    ⟨by dsimp; infer_instance, MorphismProperty.comp_mem _ _ _ F₂.property.2 F₁.property.2⟩,
    ⟨h₃, fun 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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
⊢ IsIso (F₁.obj (P := cofFib f).π.f i)

Tactic:
have := h₂ 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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this : IsIso (F₁.obj (P := cofFib f).π.f 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 ℤ
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₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this : IsIso (F₁.obj (P := cofFib f).π.f i)
⊢ IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i)

Tactic:
have := h₄ i (by lia)
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this_1 : IsIso (F₁.obj (P := cofFib f).π.f i)
this : IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i)
dsimp : IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i ≫ F₁.obj (P := cofFib f).π.f i)
⊢ IsIso (X :=
    (Factorisation.mid (f := f)
          (ObjectProperty.FullSubcategory.obj (P := cofFib f)
            (ObjectProperty.FullSubcategory.mk (P := cofFib f)
              { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid,
                ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
                π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ :
                Factorisation f }
              ⋯))).X
      i)
    (Hom.f
      (Factorisation.π
        (ObjectProperty.FullSubcategory.obj (P := cofFib f)
          (ObjectProperty.FullSubcategory.mk (P := cofFib f)
            { mid := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).mid,
              ι := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι,
              π := F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π ≫ F₁.obj (P := cofFib f).π, ι_π := ⋯ }
            ⋯)))
      i)

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
inst_3 : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right :
  Mono (X := homology K n₁) (Y := homology F₁.obj (P := cofFib f).mid n₁) (homologyMap F₁.obj (P := cofFib f).ι n₁)
F₂ : (cofFib F₁.obj (P := cofFib f).ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
i : ℤ
hi : i ≤ n₀
this_1 : IsIso (F₁.obj (P := cofFib f).π.f i)
this : IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i)
⊢ IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i ≫ F₁.obj (P := cofFib f).π.f i)

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 : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
⊢ Mono { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ : Factorisation 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
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
dsimp : QuasiIsoAt f i
⊢ QuasiIsoAt
    (ObjectProperty.FullSubcategory.obj (P := cofFib f)
        (ObjectProperty.FullSubcategory.mk (P := cofFib f) { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ : Factorisation f }
          ⋯)).ι
    i

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
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
rw : IsIso (X := homology K i) (Y := homology L i) (homologyMap f i)
⊢ QuasiIsoAt f 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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
hX : IsZero.{v_1, u_1} (homology K i)
hY : IsZero.{v_1, u_1} (homology L i)
⊢ IsIso (X := homology K i) (Y := homology L i) (homologyMap f i)

Tactic:
apply IsZero.isIso

Premises used: CategoryTheory.Limits.IsZero.isIso
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
hX : ExactAt K i
⊢ IsZero.{v_1, u_1} (homology K 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
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ ExactAt K i

Tactic:
exactAt_of_isGE _ (n + 1) i

Premises used: CochainComplex.exactAt_of_isGE, HAdd.hAdd, 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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ ExactAt K i

Tactic:
exact exactAt_of_isGE _ (n + 1) i

Premises used: CochainComplex.exactAt_of_isGE, HAdd.hAdd, 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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
hY : ExactAt L i
⊢ IsZero.{v_1, u_1} (homology L 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
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ ExactAt L i

Tactic:
exactAt_of_isGE _ (n + 1) i

Premises used: CochainComplex.exactAt_of_isGE, HAdd.hAdd, 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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n : ℤ
inst_4 : K.IsStrictlyGE (n + 1)
inst_5 : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ ExactAt L i

Tactic:
exact exactAt_of_isGE _ (n + 1) i

Premises used: CochainComplex.exactAt_of_isGE, HAdd.hAdd, 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 ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
obtain :
  ∀ (F₁₂ : (cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).FullSubcategory) (h₁ : quasiIsoLE n₁ F₁₂)
    (h₂ : isIsoLE n₀ F₁₂),
    ∃ (F' : CofFibFactorizationQuasiIsoLE f n₁) (g : F'.obj (P := quasiIsoLE n₁) ⟶ F.obj (P := quasiIsoLE n₀)),
      ∀ i ≤ n₀, IsIso (g.hom.h.f i)
⊢ ∃ (F' : CofFibFactorizationQuasiIsoLE f n₁) (g : F'.obj (P := quasiIsoLE n₁) ⟶ F.obj (P := quasiIsoLE n₀)),
    ∀ i ≤ n₀, IsIso (g.hom.h.f i)

Tactic:
obtain ⟨F₁₂, h₁, h₂⟩ := step F.obj.obj.ι n₀ n₁ F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Factorisation.ι, _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₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
dsimp : Mono F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).ι
⊢ Mono (Y :=
    Factorisation.mid (f := f)
      { mid := F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).mid,
        ι := F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).ι,
        π :=
          F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).π ≫
            F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).π,
        ι_π := ⋯ })
    (Factorisation.ι
      { mid := F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).mid,
        ι := F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).ι,
        π :=
          F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).π ≫
            F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).π,
        ι_π := ⋯ })

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₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
⊢ Mono F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib 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
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
⊢ ∃ (F' : CofFibFactorizationQuasiIsoLE f n₁) (g : F'.obj (P := quasiIsoLE n₁) ⟶ F.obj (P := quasiIsoLE n₀)),
    ∀ i ≤ n₀, IsIso (g.hom.h.f i)

Tactic:
exact ⟨.mk (.mk { mid := F₁₂.obj.mid, ι := F₁₂.obj.ι, π := F₁₂.obj.π ≫ F.obj.obj.π }
    ⟨by dsimp; infer_instance,
      MorphismProperty.comp_mem _ _ _ F₁₂.property.2 F.obj.property.2⟩) h₁,
      ObjectProperty.homMk { h := F₁₂.obj.π }, 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₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ IsIso (X := (F.next n₁ hn₁).obj (P := quasiIsoLE n₁).obj (P := cofFib f).mid.X i)
    (Hom.f (Factorisation.Hom.h (InducedCategory.Hom.hom (F.fromNext n₁ hn₁))) i)

Tactic:
(F.exists_next n₁ hn₁).choose_spec.choose_spec i hi

Premises used: Exists.choose_spec, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.exists_next
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
q : ℕ
⊢ n₀ + (↑q : ℤ) + 1 = n₀ + (↑(q + 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
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + (↑q₁ : ℤ)
inr :
  ∀
    (this :
      ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
        IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i))
    (hq' : ¬q₁ + 1 = q₂), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
wlog :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
wlog hq' : q₁ + 1 = q₂ generalizing q₁ q₂
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + (↑q₁ : ℤ)
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
inr : ∀ (k : ℕ) (hk : q₁ + k = q₂), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest hq

Premises used: Nat.le.dest
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + (↑q₁ : ℤ)
hk : q₁ + 0 = q₂
⊢ q₁ = q₂

Tactic:
simpa using hk
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + (↑q₁ : ℤ)
hk : q₁ + 0 = q₂
inr : ∀ (hq : q₁ ≤ q₁) (hk : q₁ + 0 = q₁), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
obtain rfl : q₁ = q₂ := by simpa using hk

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁
hk : q₁ + 0 = q₁
inr : IsIso.{v_1, u_1} (𝟙 (((functor f n₀).obj (op q₁)).obj (P := cofFib f).mid.X i))
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
simp only [homOfLE_refl, op_id, CategoryTheory.Functor.map_id,
        ObjectProperty.FullSubcategory.id_hom, Factorisation.id_h, id_f]

Premises used: CategoryTheory.Factorisation.id_h, CategoryTheory.homOfLE_refl, HomologicalComplex.id_f, CategoryTheory.Functor.map_id, CategoryTheory.ObjectProperty.FullSubcategory.id_hom, CategoryTheory.op_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
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁
hk : q₁ + 0 = q₁
⊢ IsIso.{v_1, u_1} (𝟙 (((functor f n₀).obj (op q₁)).obj (P := cofFib f).mid.X i))

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₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hq' : q₁ + 1 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
k : ℕ
h :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hk : q₁ + k = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + (↑q₁ : ℤ)
hk : q₁ + (k + 1) = q₂
⊢ q₁ ≤ q₁ + k

Tactic:
lia