awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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 sorry)))
          ((functor f n₀).map (Quiver.Hom.op (homOfLE sorry))))))
    i)
Tactic: rw [← homOfLE_comp (show q₁ ≤ q₁ + k by lia) (show q₁ + k ≤ q₂ by lia),
        op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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)
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)
Cleared hypotheses: q₁, q₂, hq, hi, k, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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)
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)
Cleared hypotheses: q₁, q₂, hq, hi, k, hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have subst : ∀ (hq : q₁ ≤ q₁ + 1), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
Tactic: subst hq'
Cleared hypotheses: q₂, hq, hq'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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)
Tactic: dsimp [functor]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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.{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)
have 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)
Tactic: rw [Functor.ofSequence_map_homOfLE_succ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 = Hom.f (midπ f n₀ q₁) i
have 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
Tactic: rw [← midπ_w f n₀ q₁ q₂ hq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 (ι f n₀) i ≫ Hom.f (midπ f n₀ q) i = ((functor f n₀).obj (op q)).obj (P := cofFib f).ι.f i
have 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)
Tactic: rw [← ι_midπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 = Hom.f (π f n₀) i
have 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
Tactic: rw [← midπ_π f n₀ q]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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)
⊢ (mid f n₀).IsStrictlyGE (n₀ + 1)
have rw : ∀ (i : ℤ), autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mid f n₀).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
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
⊢ IsZero.{v_1, u_1} ((mid f n₀).X i)
have 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)
Tactic: have := isIso_midπ_f f n₀ 0 i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℤ
⊢ Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)
have obtain : ∀ (q : ℕ), IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i) → Mono (Y := (mid f n₀).X i) (Hom.f (ι f n₀) i)
Tactic: obtain ⟨q, _⟩ : ∃ (q : ℕ), IsIso ((midπ f n₀ q).f i) :=
      ⟨(i - n₀).natAbs, isIso_midπ_f f n₀ _ i⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℤ
⊢ QuasiIsoAt (L := mid f n₀) (ι f n₀) i
have obtain : ∀ (q : ℕ) (hq : i + 1 ≤ n₀ + (↑q : ℤ)), QuasiIsoAt (L := mid f n₀) (ι f n₀) i
Tactic: obtain ⟨q, hq⟩ : ∃ (q : ℕ), i + 1 ≤ n₀ + q := ⟨(i + 1 - n₀).natAbs, by lia⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
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 : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
⊢ QuasiIsoAt (L := mid f n₀) (ι f n₀) i
have this : QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i
Tactic: have := quasiIsoAt_midπ f n₀ q i hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℕ
hq : i + 1 ≤ n₀ + (↑q : ℤ)
this : QuasiIsoAt (K := mid f n₀) (midπ f n₀ q) i
⊢ QuasiIsoAt (L := mid f n₀) (ι f n₀) i
have rw : QuasiIsoAt ((functor f n₀).obj (op q)).obj (P := cofFib f).ι i
Tactic: rw [← quasiIsoAt_iff_comp_right _ (midπ f n₀ q), ι_midπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℤ
⊢ epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)
have obtain : ∀ (q : ℕ) (hq : i ≤ n₀ + (↑q : ℤ)), epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)
Tactic: obtain ⟨q, hq⟩ : ∃ (q : ℕ), i ≤ n₀ + q := ⟨(i - n₀).natAbs, by lia⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
⊢ epiWithInjectiveKernel (X := (mid f n₀).X i) (Hom.f (π f n₀) i)
have rw : epiWithInjectiveKernel (Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i)
Tactic: rw [← midπ_π_f f n₀ q]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
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 : ℕ
hq : i ≤ n₀ + (↑q : ℤ)
⊢ epiWithInjectiveKernel (Hom.f (midπ f n₀ q) i ≫ ((functor f n₀).obj (op q)).obj (P := cofFib f).π.f i)
have this : IsIso (X := (mid f n₀).X i) (Hom.f (midπ f n₀ q) i)
Tactic: have := isIso_midπ_f f n₀ q i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : L.IsStrictlyGE n
inst_5 : Mono f
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f
have obtain : ∀ (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE (n + 1)],
  ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE (n + 1)) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f
Tactic: obtain ⟨n, rfl⟩ : ∃ (q : ℤ), n = q + 1 := ⟨n - 1, by simp⟩
Cleared hypotheses: n, inst_3, inst_4
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f
have this : K.IsStrictlyGE n
Tactic: have : K.IsStrictlyGE n := K.isStrictlyGE_of_ge n (n + 1) (by lia)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f
have obtain : ∀ (L' : CochainComplex.{v_1, u_1, 0} C ℤ),
  L'.IsStrictlyGE n →
    ∀ (i : K ⟶ L') (p : L' ⟶ L),
      Mono i →
        ∀ (hp : degreewiseEpiWithInjectiveKernel p),
          QuasiIso p →
            ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
              Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = i ≫ p
Tactic: obtain ⟨L', _, i, p, _, hp, _, rfl⟩ := cm5b f n
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (goal)
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 : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex.{v_1, u_1, 0} C ℤ
w : L'.IsStrictlyGE n
i : K ⟶ L'
p : L' ⟶ L
w_1 : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w_2 : QuasiIso p
⊢ ∃ (K' : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'.IsStrictlyGE n) (ι : K ⟶ K') (π : K' ⟶ L),
    Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = i ≫ p
have obtain : ∀ (K' : CochainComplex.{v_1, u_1, 0} C ℤ),
  K'.IsStrictlyGE n →
    ∀ (ι : K ⟶ K') (π : K' ⟶ L'),
      Mono ι →
        QuasiIso ι →
          ∀ (hπ : degreewiseEpiWithInjectiveKernel π),
            Mono (ι ≫ π) →
              ∃ (K'_1 : CochainComplex.{v_1, u_1, 0} C ℤ) (_ : K'_1.IsStrictlyGE n) (ι_1 : K ⟶ K'_1) (π_1 : K'_1 ⟶ L),
                Mono ι_1 ∧ QuasiIso ι_1 ∧ degreewiseEpiWithInjectiveKernel π_1 ∧ ι_1 ≫ π_1 = (ι ≫ π) ≫ p
Tactic: obtain ⟨K', _, ι, π, _, _, hπ, rfl⟩ := cm5a_cof i n
Cleared hypotheses: i, w_1
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
⊢ Injective.{v_1, u_1} ((I K).X n)
have dsimp : Injective.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE n
⊢ (I K).IsStrictlyGE n
have rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((I K).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
⊢ (mappingCone (𝟙 (I K)) ⊞ L).IsStrictlyGE n
have rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mappingCone (𝟙 (I K)) ⊞ L).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((mappingCone (𝟙 (I K)) ⊞ L).X i)
have refine : IsZero.{v_1, u_1}
  (biprod.{v_1, u_1} (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) (mappingCone (𝟙 (I K))))
    (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) L))
Tactic: refine IsZero.of_iso ?_ ((HomologicalComplex.eval C (ComplexShape.up ℤ) i).mapBiprod _ _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1}
    (biprod.{v_1, u_1} (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) (mappingCone (𝟙 (I K))))
      (Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) i) L))
have simp : (IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1))) ∧
    IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
  IsZero.{v_1, u_1} (L.X i)
Tactic: simp only [HomologicalComplex.eval_obj, biprod_isZero_iff, mappingCone.isZero_X_iff, I_X]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ (IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1))) ∧
      IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
    IsZero.{v_1, u_1} (L.X i)
have refine_1 : IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1)))
Tactic: refine ⟨⟨?_, ?_⟩, L.isZero_of_isStrictlyGE n i hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
inst_3 : K.IsStrictlyGE (n + 1)
inst_4 : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
refine_1 : IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1)))
⊢ (IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X (i + 1))) ∧
      IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))) ∧
    IsZero.{v_1, u_1} (L.X i)
have refine_2 : IsZero.{v_1, u_1} (Injective.under.{v_1, u_1} (K.X i))
Tactic: refine ⟨⟨?_, ?_⟩, L.isZero_of_isStrictlyGE n i hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
⊢ Eq.{v_1 + 1} (α := HomComplex.Cochain K (I K) 2)
    (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ K.d p q ≫ Injective.ι (K.X q))) 0
have h : ∀ (p q : ℤ) (hpq : p + 2 = q),
  Eq.{v_1 + 1} (α := K.X p ⟶ (I K).X q)
    (HomComplex.Cochain.v
      (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ K.d p q ≫ Injective.ι (K.X q))) p q hpq)
    (HomComplex.Cochain.v 0 p q hpq)
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ epiWithInjectiveKernel (X := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f (p K L) n)
have rw : ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
  f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
  Nonempty.{v_1 + 1}
    { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f, g := HomologicalComplex.Hom.f (p K L) n,
        zero := w : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: rw [epiWithInjectiveKernel_iff]