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
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 ⋯)
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have 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 := sorry :
            ShortComplex.{v_1, u_1} C }.f
        sorry)),
  QuasiIsoAt (L := mid f n) (ι f n) n
Tactic: have h₂ := (CochainComplex.homologyMap_exact₂_of_distTriang _
      (DerivedCategory.mappingCocone_triangle_distinguished (α f n)) n).fIsKernel
-- 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 : ℤ
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
      ⋯)
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have this₁ : 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]
-- 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 : ℤ
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
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have inr : IsIso (h₁.conePointUniqueUpToIso h₂).hom
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap, this]
-- 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₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
⊢ ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F
have 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
Tactic: obtain ⟨F₁, h₁, h₂, _⟩ := step₁ f n₀ n₁ hf
-- 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₀ 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).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F
have 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
Tactic: obtain ⟨F₂, h₃, h₄⟩ := step₂ F₁.obj.ι n₀ n₁ h₁
-- 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₀ 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 (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).π, ι_π := ⋯ })
have dsimp : Mono F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).ι
Tactic: dsimp
-- 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₀ 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₂
⊢ ∃ (F : (cofFib f).FullSubcategory), quasiIsoLE n₁ F ∧ isIsoLE n₀ F
have 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).π, ι_π := sorry :
                Factorisation f }
              sorry))).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).π, ι_π := sorry }
            sorry)))
      i)
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 ↦ ?_⟩⟩
-- 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₀ 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 (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)
have this : IsIso (F₁.obj (P := cofFib f).π.f i)
Tactic: have := h₂ i hi
-- 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₀ 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 (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)
have this₁ : IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i)
Tactic: have := h₄ i (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₀ 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 (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)
have dsimp : IsIso (F₂.obj (P := cofFib F₁.obj (P := cofFib f).ι).π.f i ≫ F₁.obj (P := cofFib f).π.f i)
Tactic: dsimp
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ QuasiIsoAt
    (ObjectProperty.FullSubcategory.obj (P := cofFib f)
        (ObjectProperty.FullSubcategory.mk (P := cofFib f) { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ : Factorisation f }
          ⋯)).ι
    i
have dsimp : QuasiIsoAt f i
Tactic: dsimp
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ QuasiIsoAt f i
have rw : IsIso (X := homology K i) (Y := homology L i) (homologyMap f i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ IsIso (X := homology K i) (Y := homology L i) (homologyMap f i)
have hX : IsZero.{v_1, u_1} (homology K i)
Tactic: apply IsZero.isIso
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
hX : IsZero.{v_1, u_1} (homology K i)
⊢ IsIso (X := homology K i) (Y := homology L i) (homologyMap f i)
have hY : IsZero.{v_1, u_1} (homology L i)
Tactic: apply IsZero.isIso
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ IsZero.{v_1, u_1} (homology K i)
have hX : ExactAt K i
Tactic: rw [← exactAt_iff_isZero_homology]
-- 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 : ℤ
hi : i ≤ n + (↑0 : ℤ)
⊢ IsZero.{v_1, u_1} (homology L i)
have hY : ExactAt L i
Tactic: rw [← exactAt_iff_isZero_homology]
-- 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₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ ∃ (F' : CofFibFactorizationQuasiIsoLE f n₁) (g : F'.obj (P := quasiIsoLE n₁) ⟶ F.obj (P := quasiIsoLE n₀)),
    ∀ i ≤ n₀, IsIso (g.hom.h.f i)
have 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)
Tactic: obtain ⟨F₁₂, h₁, h₂⟩ := step F.obj.obj.ι n₀ n₁ F.property
-- 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₀ : ℤ
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 (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).π,
        ι_π := ⋯ })
have dsimp : Mono F₁₂.obj (P := cofFib F.obj (P := quasiIsoLE n₀).obj (P := cofFib f).ι).ι
Tactic: dsimp
-- 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₁ : ℤ)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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)
Tactic: wlog hq' : q₁ + 1 = q₂ generalizing q₁ 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)
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)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have 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)
Tactic: wlog hq' : q₁ + 1 = q₂ generalizing q₁ q₂
Cleared hypotheses: q₁, q₂, hq, hi
-- 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)
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have inr : ∀ (k : ℕ) (hk : q₁ + k = q₂), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
Tactic: obtain ⟨k, hk⟩ := Nat.le.dest 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 : ℤ
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₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have inr : ∀ (hq : q₁ ≤ q₁) (hk : q₁ + 0 = q₁), IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
Tactic: obtain rfl : q₁ = q₂ := by simpa using hk
Cleared hypotheses: q₂, hq, 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 : ℤ
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 (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
have inr : IsIso.{v_1, u_1} (𝟙 (((functor f n₀).obj (op q₁)).obj (P := cofFib f).mid.X i))
Tactic: simp only [homOfLE_refl, op_id, CategoryTheory.Functor.map_id,
        ObjectProperty.FullSubcategory.id_hom, Factorisation.id_h, id_f]