awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Mono f
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left₁ : IsIso φ.τ₂
⊢ (homologyShortComplex f n).Exact
have right : Epi φ.τ₁
Tactic: obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩
-- 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 : Mono f
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := homology K n) (X₂ := homology L n) (X₃ := homology (cokernel f) n) (homologyMap f n)
    (homologyMap (cokernel.π f) n) ⋯
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
left : Mono φ.τ₃
left_1 : IsIso φ.τ₂
right : Epi φ.τ₁
⊢ (homologyShortComplex f n).Exact
have rw : T.Exact
Tactic: rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ]
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
⊢ (cokernel f).IsGE n
have rw : ∀ i < n, ExactAt (cokernel f) i
Tactic: rw [isGE_iff]
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ ExactAt (cokernel f) i
have rw : IsZero.{v_1, u_1} (homology (cokernel f) 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} (homology (cokernel f) i)
have refine_1 : { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology i,
      X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
      X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology (i + 1),
      f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).g i, g := sorry.δ i (i + 1) sorry, zero := sorry :
      ShortComplex.{v_1, u_1} C }.f =
  0
Tactic: refine ((shortExact f).homology_exact₃ i (i + 1) (by simp)).isZero_X₂ ?_ ?_
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
refine_1 :
  { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f =
    0
⊢ IsZero.{v_1, u_1} (homology (cokernel f) i)
have refine_2 : { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology i,
      X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
      X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology (i + 1),
      f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).g i, g := sorry.δ i (i + 1) sorry, zero := sorry :
      ShortComplex.{v_1, u_1} C }.g =
  0
Tactic: refine ((shortExact f).homology_exact₃ i (i + 1) (by simp)).isZero_X₂ ?_ ?_
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f =
    0
have this : QuasiIsoAt f i
Tactic: have := hf i 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
this : QuasiIsoAt f i
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.f =
    0
have refine_1 : Epi
  { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology i,
      X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology i,
      X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
      f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).f i,
      g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).g i, zero := sorry :
      ShortComplex.{v_1, u_1} C }.f
Tactic: rw [← ((shortExact f).homology_exact₂ i).epi_f_iff]
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).g i, g := ⋯.δ i (i + 1) ⋯, zero := ⋯ :
        ShortComplex.{v_1, u_1} C }.g =
    0
have refine_2 : Mono
  { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
      X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology (i + 1),
      X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology (i + 1),
      f := sorry.δ i (i + 1) sorry, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).f (i + 1),
      zero := sorry : ShortComplex.{v_1, u_1} C }.g
Tactic: rw [← ((shortExact f).homology_exact₁ i (i + 1) (by simp)).mono_g_iff]
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have pos : ∀ (hi' : i + 1 < n),
  Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology (i + 1),
        f := sorry.δ i (i + 1) sorry, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).f (i + 1),
        zero := sorry : ShortComplex.{v_1, u_1} C }.g
Tactic: by_cases hi' : i + 1 < n
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
pos :
  ∀ (hi' : i + 1 < n),
    Mono
      { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
          X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
          X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
          f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have neg : ∀ (hi' : ¬i + 1 < n),
  Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := sorry }.X₂.homology (i + 1),
        f := sorry.δ i (i + 1) sorry, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry).f (i + 1),
        zero := sorry : ShortComplex.{v_1, u_1} C }.g
Tactic: by_cases hi' : i + 1 < n
-- 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have this : QuasiIsoAt f (i + 1)
Tactic: have := hf (i + 1) (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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
Tactic: obtain rfl : n = i + 1 := by lia
Cleared hypotheses: n, hf, inst_3, hi, 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have inst : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
Tactic: obtain rfl : n = i + 1 := by lia
Cleared hypotheses: n, hf, inst_3, hi, hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
inst : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have hi₁ : i < i + 1
Tactic: obtain rfl : n = i + 1 := by lia
Cleared hypotheses: n, hf, inst_4, hi, hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5a (hypothesis)
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : Abelian.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
hf₁ : ∀ i_1 < i + 1, QuasiIsoAt f i_1
inst : Mono (X := homology K (i + 1)) (Y := homology L (i + 1)) (homologyMap f (i + 1))
hi₁ : i < i + 1
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯, g := homologyMap (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯).f (i + 1),
        zero := ⋯ : ShortComplex.{v_1, u_1} C }.g
have hi'₁ : ¬i + 1 < i + 1
Tactic: obtain rfl : n = i + 1 := by lia
Cleared hypotheses: n, hf, inst_4, hi, 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_2 : Mono f
inst_3 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
⊢ QuasiIso (L := (cokernel f).truncGE n) ((cokernel f).πTruncGE n)
have rw : (cokernel f).IsGE n
Tactic: rw [quasiIso_πTruncGE_iff]
-- 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)
q : ℤ
hq : q ≤ n
⊢ QuasiIsoAt (L := mid f n) (ι f n) q
have inl : ∀ (hq : q < n), QuasiIsoAt (L := mid f n) (ι f n) q
Tactic: obtain hq | rfl := hq.lt_or_eq'
-- 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)
q : ℤ
hq : q ≤ n
inl : ∀ (hq : q < n), QuasiIsoAt (L := mid f n) (ι f n) q
⊢ QuasiIsoAt (L := mid f n) (ι f n) q
have inr : ∀ (hq : n ≤ n), QuasiIsoAt (L := mid f n) (ι f n) n
Tactic: obtain hq | rfl := hq.lt_or_eq'
Cleared hypotheses: q, hq
-- 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)
q : ℤ
hq_1 : q ≤ n
hq : q < n
⊢ QuasiIsoAt (L := mid f n) (ι f n) q
have this : QuasiIsoAt (K := mid f n) (π f n) q
Tactic: have := quasiIsoAt_π f n 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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
q : ℤ
hq_1 : q ≤ n
hq : q < n
this : QuasiIsoAt (K := mid f n) (π f n) q
⊢ QuasiIsoAt (L := mid f n) (ι f n) q
have inl : QuasiIsoAt f q
Tactic: rw [← quasiIsoAt_iff_comp_right _ (π f n), mappingCocone.lift_fst]
-- 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
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have this : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
Tactic: have := mono_homologyMap_π f n n (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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst_3 : Mono f
inst_4 : Mono (X := homology K n) (Y := homology L n) (homologyMap f n)
hq : n ≤ n
this : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
⊢ Mono (X := homology (mappingCocone.triangle (L := S f n) (α f n)).obj₁ n) (Y :=
    homology (mappingCocone.triangle (L := S f n) (α f n)).obj₂ n)
    (homologyMap (mappingCocone.triangle (L := S f n) (α f n)).mor₁ n)
have dsimp : Mono (X := homology (mappingCocone (L := S f n) (α f n)) n) (Y := homology L n)
  (homologyMap (mappingCocone.fst (α f n)) n)
Tactic: dsimp
-- 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 : Mono (X := homology (mid f n) n) (Y := homology L n) (homologyMap (π f n) n)
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have 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)
Tactic: have : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n) :=
      by dsimp; infer_instance
-- 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)
⊢ QuasiIsoAt (L := mid f n) (ι f n) n
have inr : ∀ (h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f sorry)), QuasiIsoAt (L := mid f n) (ι f n) n
Tactic: have h₁ := (exact_homologyShortComplex f n).fIsKernel