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₀ : ℤ
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₁ + k ≤ q₂

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
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₂
inr :
  IsIso (X := ((functor f n₀).obj (op q₂)).obj (P := cofFib f).mid.X i) (Y :=
    ((functor f n₀).obj (op q₁)).obj (P := cofFib f).mid.X i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := (functor f n₀).obj (op (q₁ + k))) ((functor f n₀).map (Quiver.Hom.op (homOfLE ⋯)))
            ((functor f n₀).map (Quiver.Hom.op (homOfLE ⋯))))))
      i)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
rw [← homOfLE_comp (show q₁ ≤ q₁ + k by lia) (show q₁ + k ≤ q₂ by lia),
        op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_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
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₂
⊢ i ≤ n₀ + (↑(q₁ + k) : ℤ)

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)
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₁ + k + 1 = q₂

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
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₂
⊢ i ≤ n₀ + (↑q₁ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
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₂
⊢ IsIso (X := ((functor f n₀).obj (op q₂)).obj (P := cofFib f).mid.X i) (Y :=
    ((functor f n₀).obj (op q₁)).obj (P := cofFib f).mid.X i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := (functor f n₀).obj (op (q₁ + k))) ((functor f n₀).map (Quiver.Hom.op (homOfLE ⋯)))
            ((functor f n₀).map (Quiver.Hom.op (homOfLE ⋯))))))
      i)

Tactic:
exact IsIso.comp_isIso' (this _ (by lia) (by lia)) (h _ (by lia) rfl)

Premises used: CategoryTheory.IsIso.comp_isIso', 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)
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)
k : ℕ
hk : q₁ + k = q₂
inr :
  ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂) (hi : i ≤ n₀ + (↑q₁ : ℤ)) (hk : q₁ + 0 = q₂),
    IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
inr₁ :
  ∀ (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₂),
    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:
induction k generalizing q₁ q₂ with
    | zero =>
      obtain rfl : q₁ = q₂ := by simpa using hk
      simp only [homOfLE_refl, op_id, CategoryTheory.Functor.map_id,
        ObjectProperty.FullSubcategory.id_hom, Factorisation.id_h, id_f]
      infer_instance
    | succ k h =>
      rw [← homOfLE_comp (show q₁ ≤ q₁ + k by lia) (show q₁ + k ≤ q₂ by lia),
        op_comp, Functor.map_comp]
      exact IsIso.comp_isIso' (this _ (by lia) (by lia)) (h _ (by lia) rfl)

Premises used: CategoryTheory.op_comp, CategoryTheory.Factorisation.id_h, CategoryTheory.homOfLE_refl, HomologicalComplex.id_f, CategoryTheory.Functor.map_id, CategoryTheory.homOfLE_comp, CategoryTheory.Functor.map_comp, HomologicalComplex.zero, rfl, 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 : ℤ
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq' : q₁ + 1 = q₂
subst : ∀ (hq : q₁ ≤ q₁ + 1), 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:
subst 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
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁ + 1
dsimp :
  IsIso.{v_1, u_1} (C := C) (X :=
    (ObjectProperty.FullSubcategory.obj (P := quasiIsoLE (n₀ + HAdd.hAdd (α := ℤ) (↑q₁ : ℤ) 1))
                (CofFibFactorizationQuasiIsoLE.sequence f n₀ (q₁ + 1))).obj
            (P := cofFib f).mid.X
      i)
    (Y :=
    (CofFibFactorizationQuasiIsoLE.sequence f n₀ q₁).obj (P := quasiIsoLE (n₀ + (↑q₁ : ℤ))).obj (P := cofFib f).mid.X i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (Quiver.Hom.unop
            (CategoryTheory.Functor.map
              (Functor.ofSequence (X := fun (q : ℕ) ↦
                op ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj (P := quasiIsoLE (n₀ + (↑q : ℤ)))))
                fun (q : ℕ) ↦ Quiver.Hom.op (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q))
              (homOfLE hq)))))
      i)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
dsimp [functor]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor
-- 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 : ℤ
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁ + 1
rw :
  IsIso (X :=
    (ObjectProperty.FullSubcategory.obj (P := quasiIsoLE (n₀ + HAdd.hAdd (α := ℤ) (↑q₁ : ℤ) 1))
                (CofFibFactorizationQuasiIsoLE.sequence f n₀ (q₁ + 1))).obj
            (P := cofFib f).mid.X
      i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (Quiver.Hom.unop (Quiver.Hom.op (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q₁)))))
      i)
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    (ObjectProperty.FullSubcategory.obj (P := quasiIsoLE (n₀ + HAdd.hAdd (α := ℤ) (↑q₁ : ℤ) 1))
                (CofFibFactorizationQuasiIsoLE.sequence f n₀ (q₁ + 1))).obj
            (P := cofFib f).mid.X
      i)
    (Y :=
    (CofFibFactorizationQuasiIsoLE.sequence f n₀ q₁).obj (P := quasiIsoLE (n₀ + (↑q₁ : ℤ))).obj (P := cofFib f).mid.X i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (Quiver.Hom.unop
            (CategoryTheory.Functor.map
              (Functor.ofSequence (X := fun (q : ℕ) ↦
                op ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj (P := quasiIsoLE (n₀ + (↑q : ℤ)))))
                fun (q : ℕ) ↦ Quiver.Hom.op (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q))
              (homOfLE hq)))))
      i)

Tactic:
rw [Functor.ofSequence_map_homOfLE_succ]

Premises used: CategoryTheory.Functor.ofSequence_map_homOfLE_succ
-- 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 : ℤ
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁ + 1
⊢ IsIso (X :=
    (ObjectProperty.FullSubcategory.obj (P := quasiIsoLE (n₀ + HAdd.hAdd (α := ℤ) (↑q₁ : ℤ) 1))
                (CofFibFactorizationQuasiIsoLE.sequence f n₀ (q₁ + 1))).obj
            (P := cofFib f).mid.X
      i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (Quiver.Hom.unop (Quiver.Hom.op (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q₁)))))
      i)

Tactic:
CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_f _ _ _ _ hi

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_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
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ : ℕ
hi : i ≤ n₀ + (↑q₁ : ℤ)
hq : q₁ ≤ q₁ + 1
⊢ IsIso (X :=
    (ObjectProperty.FullSubcategory.obj (P := quasiIsoLE (n₀ + HAdd.hAdd (α := ℤ) (↑q₁ : ℤ) 1))
                (CofFibFactorizationQuasiIsoLE.sequence f n₀ (q₁ + 1))).obj
            (P := cofFib f).mid.X
      i)
    (Hom.f
      (Factorisation.Hom.h
        (InducedCategory.Hom.hom
          (Quiver.Hom.unop (Quiver.Hom.op (CofFibFactorizationQuasiIsoLE.toSequenceNext f n₀ q₁)))))
      i)

Tactic:
exact CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_f _ _ _ _ hi

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.isIso_fromNext_hom_h_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
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
h : i ≤ n₀ + (↑q : ℤ)
x : ℕᵒᵖ
x_1 : x ⟶ op q
⊢ i ≤ n₀ + (↑q : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ HasLimit (cochainComplexFunctor f n₀ ⋙ eval C (ComplexShape.up ℤ) i)

Tactic:
(isEventuallyConstantTo f n₀ i (n₀ - i).natAbs).hasLimit

Premises used: HSub.hSub, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isEventuallyConstantTo, Int.natAbs, CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit
-- 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₂
⊢ midπ f n₀ q₂ ≫ ((functor f n₀).map (homOfLE hq).op).hom.h = midπ f n₀ q₁

Tactic:
limit.w _ _

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ, CategoryTheory.Limits.limit.w
-- 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 : ℤ
rw :
  Hom.f (midπ f n₀ q₂) i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i =
    (midπ f n₀ q₂ ≫ ((functor f n₀).map (homOfLE hq).op).hom.h).f i
⊢ Hom.f (midπ f n₀ q₂) i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i = Hom.f (midπ f n₀ q₁) i

Tactic:
rw [← midπ_w f n₀ q₁ q₂ hq]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w
-- 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 : ℤ
⊢ Hom.f (midπ f n₀ q₂) i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i =
    (midπ f n₀ q₂ ≫ ((functor f n₀).map (homOfLE hq).op).hom.h).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)
q : ℕ
i : ℤ
h : i ≤ n₀ + (↑q : ℤ)
⊢ IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)

Tactic:
isIso_π_f_of_isLimit_of_isEventuallyConstantTo _ (limit.isLimit _) _ _
    (isEventuallyConstantTo f n₀ _ _)

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isEventuallyConstantTo, CategoryTheory.Limits.limit.isLimit, HomologicalComplex.isIso_π_f_of_isLimit_of_isEventuallyConstantTo
-- 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 : ℕ
i : ℤ
h : i + 1 ≤ n₀ + (↑q : ℤ)
⊢ (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 ℤ
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 : ℕ
i : ℤ
h : i + 1 ≤ n₀ + (↑q : ℤ)
⊢ (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 ℤ
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 : ℕ
⊢ ι f n₀ ≫ midπ f n₀ q = ((functor f n₀).obj (op q)).obj (P := cofFib f).ι

Tactic:
simp [ι, midπ]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι
-- 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 : ℕ
i : ℤ
rw :
  Eq (α := K.X i ⟶ ((functor f n₀).obj (op q)).obj (P := cofFib f).mid.X i) (Hom.f (ι f n₀) i ≫ Hom.f (midπ f n₀ q) i)
    (Hom.f (ι f n₀ ≫ midπ f n₀ q) i)
⊢ Hom.f (ι f n₀) i ≫ Hom.f (midπ f n₀ q) i = ((functor f n₀).obj (op q)).obj (P := cofFib f).ι.f i

Tactic:
rw [← ι_midπ]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ
-- 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 : ℕ
i : ℤ
⊢ Eq (α := K.X i ⟶ ((functor f n₀).obj (op q)).obj (P := cofFib f).mid.X i) (Hom.f (ι f n₀) i ≫ Hom.f (midπ f n₀ q) i)
    (Hom.f (ι f n₀ ≫ midπ f n₀ q) 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)
⊢ CategoryStruct.comp (Y := mid f n₀) (ι f n₀) (π f n₀) = f

Tactic:
simp [π]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π
-- 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 : ℕ
⊢ 0 ≤ q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
q : ℕ
⊢ midπ f n₀ q ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π = π f n₀

Tactic:
simp [π, ← midπ_w_assoc f n₀ 0 q (by lia)]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w_assoc, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π, 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)
q : ℕ
i : ℤ
rw :
  Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i =
    (midπ f n₀ q ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π).f i
⊢ Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i = Hom.f (π f n₀) i

Tactic:
rw [← midπ_π f n₀ q]

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π
-- 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 : ℕ
i : ℤ
⊢ Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i =
    (midπ f n₀ q ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π).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)
rw : ∀ (i : ℤ), autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mid f n₀).X i)
⊢ (mid f n₀).IsStrictlyGE (n₀ + 1)

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.Factorizations.CM5a
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
inst_3 : Mono f
n₀ : ℤ
inst_4 : K.IsStrictlyGE (n₀ + 1)
inst_5 : L.IsStrictlyGE (n₀ + 1)
i : ℤ
hi : autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1
⊢ IsIso (X := (mid f n₀).X i) (Y := ((functor f n₀).obj (op 0)).obj (P := cofFib f).mid.X i) (Hom.f (midπ f n₀ 0) i)

Tactic:
have := isIso_midπ_f f n₀ 0 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 ℤ
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 : autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1
this :
  IsIso (X := (mid f n₀).X i) (Y := ((functor f n₀).obj (op 0)).obj (P := cofFib f).mid.X i) (Hom.f (midπ f n₀ 0) i)
⊢ IsZero.{v_1, u_1} ((mid f n₀).X i)

Tactic:
(L.isZero_of_isStrictlyGE (n₀ + 1) i).of_iso (asIso ((midπ f n₀ 0).f i))

Premises used: HomologicalComplex.Hom.f, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ, CategoryTheory.Limits.IsZero.of_iso, CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, OfNat.ofNat, CategoryTheory.asIso
-- 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 : autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1
this :
  IsIso (X := (mid f n₀).X i) (Y := ((functor f n₀).obj (op 0)).obj (P := cofFib f).mid.X i) (Hom.f (midπ f n₀ 0) i)
⊢ IsZero.{v_1, u_1} ((mid f n₀).X i)

Tactic:
exact (L.isZero_of_isStrictlyGE (n₀ + 1) i).of_iso (asIso ((midπ f n₀ 0).f i))

Premises used: HomologicalComplex.Hom.f, _private.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ, CategoryTheory.Limits.IsZero.of_iso, CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, OfNat.ofNat, CategoryTheory.asIso