awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this : HasZeroObject.{u_2, u_1} C
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)
have this₁ : (S.sc hS k sorry).HasHomology
Tactic: have := hS'.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)
have this₁ : Mono h.g'
Tactic: have := h.exact_iff_mono_g'.1 hS'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
have rw : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.p ≫ h.g'
Tactic: rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
rw : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.p ≫ h.g'
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
have rw₁ : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k sorry).g
Tactic: rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
rw : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.p ≫ h.g'
rw₁ : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
have rw₂ : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k sorry).g
Tactic: rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
rw : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.p ≫ h.g'
rw₁ : h.p ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g
rw₂ : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS k ⋯).g
⊢ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
have rw₃ : S.map' (k + 1) (k + 2) sorry sorry = (S.sc hS k sorry).g
Tactic: rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this_1 : HasZeroObject.{u_2, u_1} C
this_2 : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)
have fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = h.g'
Tactic: have fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = h.g' := by
    rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
have this : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
Tactic: have : Mono (hS.cokerToKer' k hk cc kf hcc hkf) :=
      hS.toIsComplex.mono_cokerToKer' k hk cc kf hcc hkf
    (hS.exact k)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ExactSequenceFour (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : Balanced.{u_2, u_1} C
n : ℕ
S : ComposableArrows.{u_2, u_1} C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc :
  CokernelCofork (X := S.obj ⟨k, ⋯⟩) (Y := S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
kf :
  KernelFork (X := S.obj ⟨k + 2, ⋯⟩) (Y := S.obj ⟨k + 3, ⋯⟩)
    (S.map' (k + 2) (k + 3) ⋯ ⋯ : S.obj (⟨k + 2, ⋯⟩ : Fin (n + 3 + 1)) ⟶ S.obj ⟨k + 3, ⋯⟩)
hcc : IsColimit cc
hkf : IsLimit kf
this : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
have this₁ : Epi (hS.cokerToKer' k hk cc kf hcc hkf)
Tactic: have : Epi (hS.cokerToKer' k hk cc kf hcc hkf) :=
    hS.epi_cokerToKer' k hk cc kf hcc hkf (hS.exact (k + 1))
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.Basic (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
hL : IsZero L
n : ℤ
⊢ epiWithInjectiveKernel (f.f n) ↔ Injective.{v_1, u_1} (K.X n)
have hY : IsZero.{v_1, u_1} (L.X n)
Tactic: rw [epiWithInjectiveKernel_iff_of_isZero]
-- 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₁ q : ℤ
⊢ epiWithInjectiveKernel (X := (mid K L n₁).X q) (Hom.f (π K L n₁) q)
have rw : ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mid K L n₁).X q) (w : f ≫ Hom.f (π K L n₁) q = 0),
  Nonempty.{v_1 + 1}
    { X₁ := I, X₂ := (mid K L n₁).X q, X₃ := L.X q, f := f, g := Hom.f (π K L n₁) q, zero := w :
        ShortComplex.{v_1, u_1} C }.Splitting
Tactic: rw [Abelian.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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
⊢ IsIso (X := (mid K L n₁).X i) (Hom.f (π K L n₁) i)
have refine : Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i = 𝟙 ((mid K L n₁).X i)
Tactic: refine ⟨(biprod.inr : _ ⟶ mid K L n₁).f i, ?_, 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
⊢ Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i = 𝟙 ((mid K L n₁).X i)
have rw : Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i) ∧
  Eq (α := (mid K L n₁).X i ⟶ L.X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
Tactic: rw [biprodX_ext_to_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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hi : i ≠ n₁
⊢ Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i) ∧
    Eq (α := (mid K L n₁).X i ⟶ L.X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
have left : Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
  (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
  (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i)
Tactic: constructor
-- 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₁ i : ℤ
hi : i ≠ n₁
left :
  Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
    (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
    (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i)
⊢ Eq (α := (mid K L n₁).X i ⟶ (S K n₁).X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.fst i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.fst i) ∧
    Eq (α := (mid K L n₁).X i ⟶ L.X i)
      (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
      (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
have right : Eq (α := (mid K L n₁).X i ⟶ L.X i)
  (CategoryStruct.comp (Y := (S K n₁ ⊞ L).X i) (Hom.f (π K L n₁) i ≫ Hom.f biprod.inr i) (Hom.f biprod.snd i))
  (𝟙 ((mid K L n₁).X i) ≫ Hom.f biprod.snd i)
Tactic: constructor
-- 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
have inl : ∀ (hi : i < n₀), QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
Tactic: obtain (hi | rfl) := hi.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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
inl : ∀ (hi : i < n₀), QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
have inr : ∀ (hn₁ : i + 1 = n₁) (hi : i ≤ i), QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
Tactic: obtain (hi | rfl) := hi.lt_or_eq
Cleared hypotheses: n₀, hn₁, 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
have inl : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
  (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))
Tactic: rw [quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))
have this : IsIso φ.τ₁
Tactic: have : IsIso φ.τ₁ := isIso_π_f ..
-- 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this : IsIso φ.τ₁
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))
have this₁ : IsIso φ.τ₂
Tactic: have : IsIso φ.τ₂ := isIso_π_f ..
-- 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi_1 : i ≤ n₀
hi : i < n₀
φ : Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁) ⟶
  Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) L :=
  CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁)
this_1 : IsIso φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (mid K L n₁))
    (CategoryTheory.Functor.map (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)) (π K L n₁))
have this₁ : IsIso φ.τ₃
Tactic: have : IsIso φ.τ₃ := isIso_π_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₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
have inr : IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
⊢ IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)
have this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
Tactic: have : homologyMap (biprod.inl : _ ⟶ mid K L n₁) i = 0 :=
      (ShortComplex.isZero_homology_of_isZero_X₂ _
        (isZero_single_obj_X (.up ℤ) _ _ _ (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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
⊢ IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)
have inr : CategoryStruct.comp (Y := homology L i) (homologyMap (π K L n₁) i) (homologyMap (σ K L n₁) i) =
  𝟙 (homology (mid K L n₁) i)
Tactic: refine ⟨homologyMap (σ K L 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 ℤ
inst_2 : EnoughInjectives.{v_1, u_1} C
n₁ i : ℤ
hn₁ : i + 1 = n₁
hi : i ≤ i
this : Eq.{v_1 + 1} (α := homology (S K n₁) i ⟶ homology (S K n₁ ⊞ L) i) (homologyMap biprod.inl i) 0
inr :
  CategoryStruct.comp (Y := homology L i) (homologyMap (π K L n₁) i) (homologyMap (σ K L n₁) i) =
    𝟙 (homology (mid K L n₁) i)
⊢ IsIso (X := homology (mid K L n₁) i) (Y := homology L i) (homologyMap (π K L n₁) i)
have inr₁ : CategoryStruct.comp (Y := homology (mid K L n₁) i) (homologyMap (σ K L n₁) i) (homologyMap (π K L n₁) i) =
  𝟙 (homology L i)
Tactic: refine ⟨homologyMap (σ K L n₁) i, ?_, ?_⟩
-- 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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (L := mid K L n₁) (ι f n₁) i
have this : QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
Tactic: have := quasiIsoAt_π K L n₀ n₁ hn₁ 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
inst_2 : EnoughInjectives.{v_1, u_1} C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (K := mid K L n₁) (π K L n₁) i
⊢ QuasiIsoAt (L := mid K L n₁) (ι f n₁) i
have rw : QuasiIsoAt f i
Tactic: rw [← quasiIsoAt_iff_comp_right _ (π K L 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₀_1 n₁ : ℤ
hn₁ : n₀_1 + 1 = n₁
hf : ∀ i ≤ n₀_1, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
⊢ (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
⊢ Mono (X := homology K n₁) (Y := homology (mid K L n₁) n₁) (homologyMap (ι f n₁) n₁)
have rw : ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X n₁),
  Eq (α := A ⟶ K.X (n₁ + 1)) (x₂ ≫ K.d n₁ (n₁ + 1)) 0 →
    ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
      x₂ ≫ Hom.f (ι f n₁) n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X n₀), π ≫ x₂ = x₁ ≫ K.d n₀ n₁
Tactic: rw [mono_homologyMap_iff_up_to_refinements _ n₀ n₁ (n₁ + 1) (by simp; lia) (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₀_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₁
⊢ ∃ (z₁ : A ⟶ L.X n₀), z₁ ≫ Hom.f (σ K L n₁) n₀ = y₀
have refine : (y₀ ≫ Hom.f (π K L n₁) n₀) ≫ Hom.f (σ K L n₁) n₀ = y₀ ≫ 𝟙 ((mid K L n₁).X n₀)
Tactic: refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩
-- 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 ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ Hom.f (ι f n₁) n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ (y₀ ≫ Hom.f (π K L n₁) n₀) ≫ Hom.f (σ K L n₁) n₀ = y₀ ≫ 𝟙 ((mid K L n₁).X n₀)
have this : Eq.{v_1 + 1} (α := (S K n₁).X n₀ ⟶ (S K n₁ ⊞ L).X n₀) (Hom.f biprod.inl n₀) 0
Tactic: have : (biprod.inl : _ ⟶ mid K L n₁).f n₀ = 0 :=
      (isZero_single_obj_X (.up ℤ) _ _ _ (by lia)).eq_of_src _ _