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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have obtain : ∀ (y₀ : A ⟶ L.X n₀) (hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = (y₀ ≫ Hom.f (σ K L n₁) n₀) ≫ (mid K L n₁).d n₀ n₁),
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
Tactic: obtain ⟨y₀, rfl⟩ : ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ (σ K L n₁).f n₀ = y₀ := by
    refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
    have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (by lia)).eq_of_src _ _
    simp [this, ← biprod_total_f]
Cleared hypotheses: y₀, hy₀
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = (y₀ ≫ Hom.f (σ K L n₁) n₀) ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have hy₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
Tactic: simp only [Category.assoc, Hom.comm, biprodX_ext_to_iff, biprod_lift_fst_f,
    biprod_inr_fst_f, comp_zero, biprod_lift_snd_f, biprod_inr_snd_f,
    Category.comp_id] at hy₀
Cleared hypotheses: hy₀
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
hy₀ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
Tactic: obtain ⟨h₁, h₂⟩ := hy₀
Cleared hypotheses: hy₀
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
hy₀ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
Tactic: obtain ⟨h₁, h₂⟩ := hy₀
Cleared hypotheses: hy₀
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
have rw : Eq (α := A ⟶ Injective.under.{v_1, u_1} (opcycles K n₁)) ((x₁ ≫ pOpcycles K n₁) ≫ Injective.ι (opcycles K n₁))
  (0 ≫ Injective.ι (opcycles K n₁))
Tactic: rw [← cancel_mono (Injective.ι _)]
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₁ : Eq (α := A ⟶ (S K n₁).X n₁) (x₁ ≫ Hom.f (i K n₁) n₁) 0
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have h₃ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
Tactic: replace h₁ : x₁ ≫ K.pOpcycles n₁ = 0 := by
    rw [← cancel_mono (Injective.ι _)]
    simpa [i, ← cancel_mono (singleObjXSelf (.up ℤ) n₁ _).hom] using h₁
Cleared hypotheses: 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
n₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
⊢ (ComplexShape.up ℤ).prev n₁ = n₀
have simp : n₁ - 1 = n₀
Tactic: simp
-- 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
h : Eq (α := A ⟶ K.X (n₁ + 1)) (x₁ ≫ K.d n₁ (n₁ + 1)) 0
y₀ : A ⟶ L.X n₀
h₂ : x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
h₁ : Eq (α := A ⟶ opcycles K n₁) (x₁ ≫ pOpcycles K n₁) 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
have obtain : ∀ (A₁ : C) (π : A₁ ⟶ A),
  Epi π →
    ∀ (x₀ : A₁ ⟶ K.X n₀) (hx₀ : π ≫ x₁ = x₀ ≫ K.d n₀ n₁),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁_1 : A' ⟶ K.X n₀), π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
Tactic: obtain ⟨A₁, π, _, x₀, hx₀⟩ :=
    (K.comp_pOpcycles_eq_zero_iff_up_to_refinements x₁ n₀ (by simp; lia)).1 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
n : ℤ
⊢ Mono (Y := (S f n).X n) (Hom.f (p f n) n)
have simp : Mono.{v_1, u_1} (Y := Injective.under.{v_1, u_1} (((cokernel f).truncGE n).X n))
  (Injective.ι (((cokernel f).truncGE n).X n))
Tactic: simp only [p, mkHomToSingle_f, mono_comp_iff_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
inst_2 : EnoughInjectives.{v_1, u_1} C
n i : ℤ
⊢ epiWithInjectiveKernel (X := (mid f n).X i) (Hom.f (π f n) i)
have rw : ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ (mid f n).X i) (w : f_1 ≫ Hom.f (π f n) i = 0),
  Nonempty.{v_1 + 1}
    { X₁ := I, X₂ := (mid f n).X i, X₃ := L.X i, f := f_1, g := Hom.f (π f n) i, zero := w :
        ShortComplex.{v_1, u_1} C }.Splitting
Tactic: rw [epiWithInjectiveKernel_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 i : ℤ
hi : i ≤ n
⊢ IsIso (X := (mid f n).X i) (Hom.f (π f n) i)
have refine : Hom.f (π f n) i ≫ Cochain.v (mappingCocone.inl (α f n)) i i sorry = 𝟙 ((mid f n).X i)
Tactic: refine ⟨(mappingCocone.inl (α f n)).v i i (add_zero i), ?_, by simp⟩
-- 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 q : ℤ
hq : q < n
⊢ QuasiIsoAt (K := mid f n) (π f n) q
have this : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
Tactic: have := mono_homologyMap_π f n q (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
n q : ℤ
hq : q < n
this : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
⊢ QuasiIsoAt (K := mid f n) (π f n) q
have this₁ : Epi (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
Tactic: have := epi_homologyMap_π 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 q : ℤ
hq : q < n
this_1 : Mono (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
this : Epi (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
⊢ QuasiIsoAt (K := mid f n) (π f n) q
have rw : IsIso (X := homology (mid f n) q) (Y := homology L q) (homologyMap (π f n) q)
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
n : ℤ
⊢ Eq (α := homology K n ⟶ (S f n).homology n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (α f n) n)) 0
have rw : Eq (α := homology K n ⟶ (S f n).homology n) (homologyMap (f ≫ α f n) n) 0
Tactic: rw [← homologyMap_comp, comp_α, homologyMap_zero]
-- 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 : ℤ
rw : Eq (α := homology K n ⟶ (S f n).homology n) (homologyMap (f ≫ α f n) n) 0
⊢ Eq (α := homology K n ⟶ (S f n).homology n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (α f n) n)) 0
have rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ (S f n).homology n) (homologyMap 0 n) 0
Tactic: rw [← homologyMap_comp, comp_α, homologyMap_zero]
-- 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 : ℤ
rw : Eq (α := homology K n ⟶ (S f n).homology n) (homologyMap (f ≫ α f n) n) 0
rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ (S f n).homology n) (homologyMap 0 n) 0
⊢ Eq (α := homology K n ⟶ (S f n).homology n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (α f n) n)) 0
have rw₂ : Eq.{v_1 + 1} (α := homology K n ⟶ (S f n).homology n) 0 0
Tactic: rw [← homologyMap_comp, comp_α, homologyMap_zero]
-- 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 : ℤ
⊢ Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (homologyMap (p f n) n)
have this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
Tactic: have := (S f n).isIso_homologyπ (n - 1) n (by simp) (by simp)
-- 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 : ℤ
this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
⊢ Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
have rw : Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (cyclesMap (p f n) n ≫ (S f n).homologyπ n)
Tactic: rw [homologyπ_naturality (p f n) 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
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
this : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
⊢ Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (homologyMap (p f n) n)
have this₁ : Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
  (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
Tactic: have : Mono ((truncGE (cokernel f) n).homologyπ n ≫ homologyMap (p f n) n) := by
    rw [homologyπ_naturality (p f n) n]
    infer_instance
-- 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 : ℤ
this_1 : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
this :
  Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
⊢ Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (homologyMap (p f n) n)
have this₁ : IsIso (X := cycles ((cokernel f).truncGE n) n) (homologyπ ((cokernel f).truncGE n) n)
Tactic: have := (truncGE (cokernel f) n).isIso_homologyπ (n - 1) n (by simp)
    ((isZero_of_isStrictlyGE _ n _ (by lia)).eq_of_src _ _)
-- 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 : ℤ
this_1 : IsIso (X := (S f n).cycles n) ((S f n).homologyπ n)
this_2 :
  Mono (X := cycles ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
    (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
this : IsIso (X := cycles ((cokernel f).truncGE n) n) (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n) (homologyMap (p f n) n)
have rw : Mono (X := homology ((cokernel f).truncGE n) n) (Y := (S f n).homology n)
  (inv (homologyπ ((cokernel f).truncGE n) n) ≫ homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
Tactic: rw [← IsIso.inv_hom_id_assoc ((truncGE (cokernel f) n).homologyπ n) (homologyMap (p f n) 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
inst_2 : EnoughInjectives.{v_1, u_1} C
n : ℤ
inst_3 : Mono f
⊢ Eq (α := homology K n ⟶ homology (cokernel f) n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (cokernel.π f) n)) 0
have rw : Eq (α := homology K n ⟶ homology (cokernel f) n) (homologyMap (f ≫ cokernel.π f) n) 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- 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
rw : Eq (α := homology K n ⟶ homology (cokernel f) n) (homologyMap (f ≫ cokernel.π f) n) 0
⊢ Eq (α := homology K n ⟶ homology (cokernel f) n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (cokernel.π f) n)) 0
have rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ homology (cokernel f) n) (homologyMap 0 n) 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- 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
rw : Eq (α := homology K n ⟶ homology (cokernel f) n) (homologyMap (f ≫ cokernel.π f) n) 0
rw₁ : Eq.{v_1 + 1} (α := homology K n ⟶ homology (cokernel f) n) (homologyMap 0 n) 0
⊢ Eq (α := homology K n ⟶ homology (cokernel f) n)
    (CategoryStruct.comp (Y := homology L n) (homologyMap f n) (homologyMap (cokernel.π f) n)) 0
have rw₂ : Eq.{v_1 + 1} (α := homology K n ⟶ homology (cokernel f) n) 0 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- 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.X₂ ≫ (homologyShortComplex f n).g = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n
have dsimp : Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
  (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
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
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) ⋯
⊢ Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
    (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
have rw : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n) (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
Tactic: rw [Category.id_comp, ← homologyMap_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
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) ⋯
rw : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n) (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
⊢ Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
    (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
have rw₁ : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n)
  (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
Tactic: rw [Category.id_comp, ← homologyMap_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
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) ⋯
rw : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n) (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
rw₁ :
  Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (α f n) n)
    (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
⊢ Eq (α := T.X₂ ⟶ (S f n).homology n) (𝟙 T.X₂ ≫ homologyMap (α f n) n)
    (T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n)
have rw₂ : Eq (α := T.X₂ ⟶ (S f n).homology n) (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
  (homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n)
Tactic: rw [Category.id_comp, ← homologyMap_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
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₂₃ := ⋯ }
⊢ Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁
have dsimp : Mono (X := T.X₃) (Y := (S f n).homology n) (homologyMap ((cokernel f).πTruncGE n ≫ p f n) n) ∧
  IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)
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
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₂₃ := ⋯ }
⊢ Mono (X := T.X₃) (Y := (S f n).homology n) (homologyMap ((cokernel f).πTruncGE n ≫ p f n) n) ∧
    IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)
have rw : Mono (X := T.X₃) (Y := (S f n).homology n)
    (CategoryStruct.comp (Y := homology ((cokernel f).truncGE n) n) (homologyMap ((cokernel f).πTruncGE n) n)
      (homologyMap (p f n) n)) ∧
  IsIso.{v_1, u_1} (𝟙 T.X₂) ∧ Epi.{v_1, u_1} (𝟙 T.X₁)
Tactic: rw [homologyMap_comp]
-- 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₂₃ := ⋯ }
⊢ (homologyShortComplex f n).Exact
have left : Mono φ.τ₃
Tactic: obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩
-- 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 φ.τ₃
⊢ (homologyShortComplex f n).Exact
have left₁ : IsIso φ.τ₂
Tactic: obtain ⟨_, _, _⟩ : Mono φ.τ₃ ∧ IsIso φ.τ₂ ∧ Epi φ.τ₁ := by
    dsimp [φ]
    rw [homologyMap_comp]
    exact ⟨inferInstance, inferInstance, inferInstance⟩