awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip_1 :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
⊢ sq.HasLift
have this₁ : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
Tactic: have (n : ℤ) : Injective ((kernel p).X n) :=
      Injective.of_iso
        (asIso (kernelComparison p (HomologicalComplex.eval _ _ n))).symm (hp n).2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip_1 : QuasiIso i ∨ QuasiIso p
sq_1 : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq_1 fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
sq :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
⊢ (kernel p).IsStrictlyGE d
have rw : ∀ (i : ℤ), autoParam (i < d) isStrictlyGE_iff._auto_1 → IsZero.{u_2, u_1} ((kernel p).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i_1 : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i_1)
hi_1 : Mono i_1
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip_1 : QuasiIso i_1 ∨ QuasiIso p
sq_1 : CommSq t i_1 p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i_1.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i_1) (kernel p) 1 :=
  Lifting.cocycle₁ sq_1 fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i_1)
    (hι := ⋯) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i_1) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
sq :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i_1)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
i : ℤ
hi : autoParam (i < d) isStrictlyGE_iff._auto_1
⊢ IsZero.{u_2, u_1} ((kernel p).X i)
have rw : 𝟙 ((kernel p).X i) ≫ HomologicalComplex.Hom.f (kernel.ι p) i =
  CategoryStruct.comp (Y := (kernel p).X i) 0 (HomologicalComplex.Hom.f (kernel.ι p) i)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono ((kernel.ι p).f i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip_1 : QuasiIso i ∨ QuasiIso p
sq_1 : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq_1 fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
sq :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
⊢ (kernel p).IsKInjective
have this₁ : (kernel p).IsStrictlyGE d
Tactic: have : (kernel p).IsStrictlyGE d := by
        rw [isStrictlyGE_iff]
        intro i hi
        rw [IsZero.iff_id_eq_zero, ← cancel_mono ((kernel.ι p).f i)]
        apply (X.isZero_of_isStrictlyGE d i).eq_of_tgt
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip_1 :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
⊢ sq.HasLift
have this₁ : (kernel p).IsKInjective
Tactic: have : (kernel p).IsKInjective := by
      obtain ⟨d, hd⟩ := hX
      have : (kernel p).IsStrictlyGE d := by
        rw [isStrictlyGE_iff]
        intro i hi
        rw [IsZero.iff_id_eq_zero, ← cancel_mono ((kernel.ι p).f i)]
        apply (X.isZero_of_isStrictlyGE d i).eq_of_tgt
      exact isKInjective_of_injective _ d
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip_1 :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
⊢ ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
have inl : QuasiIso i → ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
Tactic: cases hip
Cleared hypotheses: hip
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip_1 :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
inl : QuasiIso i → ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
⊢ ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
have inr : QuasiIso p → ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
Tactic: cases hip
Cleared hypotheses: hip
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
h : QuasiIso i
⊢ ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
have inl : HomologicalComplex.Acyclic (cokernel i)
Tactic: refine IsKInjective.eq_δ_of_cocycle β ?_ 0 (by simp)