awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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 p
⊢ Epi p

Tactic:
have := hp.epi
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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_3 : (kernel p).IsKInjective
h : QuasiIso p
this : Epi p
⊢ (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯).ShortExact

Tactic:
have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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_3 : (kernel p).IsKInjective
h : QuasiIso p
this_4 : Epi p
this : (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯).ShortExact
dsimp : QuasiIso p
⊢ QuasiIso (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯).g

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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_3 : (kernel p).IsKInjective
h : QuasiIso p
this_4 : Epi p
this : (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯).ShortExact
⊢ QuasiIso p

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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_3 : (kernel p).IsKInjective
h : QuasiIso p
this_4 : Epi p
this : (ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯).ShortExact
⊢ HomologicalComplex.Acyclic (kernel p)

Tactic:
exact this.acyclic_X₁ (by dsimp; infer_instance)

Premises used: CategoryTheory.ShortComplex.ShortExact.acyclic_X₁
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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
hα : δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
⊢ sq.HasLift

Tactic:
Lifting.hasLift sq _ (cokernelIsCokernel _) (kernelIsKernel _) α hα

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CochainComplex.Lifting.hasLift, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
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
hα : δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)
⊢ sq.HasLift

Tactic:
exact Lifting.hasLift sq _ (cokernelIsCokernel _) (kernelIsKernel _) α hα

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CochainComplex.Lifting.hasLift, CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A B X Y : Plus.{u_2, u_1} C
i : A ⟶ B
p : X ⟶ Y
inst_2 : Mono i
inst_3 : WeakEquivalence i
inst_4 : Fibration p
⊢ HasLiftingProperty i p

Tactic:
lifting _ _ (Or.inl inferInstance)

Premises used: inferInstance, Or.inl, _private.0.CochainComplex.Plus.modelCategoryQuillen.lifting
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A B X Y : Plus.{u_2, u_1} C
i : A ⟶ B
p : X ⟶ Y
inst_2 : Mono i
inst_3 : Fibration p
inst_4 : WeakEquivalence p
⊢ HasLiftingProperty i p

Tactic:
lifting _ _ (Or.inr inferInstance)

Premises used: inferInstance, _private.0.CochainComplex.Plus.modelCategoryQuillen.lifting, Or.inr
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
this :
  ∀ (L : CochainComplex.{u_2, u_1, 0} C ℤ) (m : ℤ) (hm : L.IsStrictlyGE m)
    (f :
      Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C))
        f)
⊢ ∀ {Y : Plus.{u_2, u_1} C} (f : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯ ⟶ Y),
    Nonempty
      (MorphismProperty.MapFactorizationData (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C))
        f)

Tactic:
⟨L, m, hm⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
this :
  ∀
    (f :
      ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
        ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (trivialCofibrations (Plus.{u_2, u_1} C))
        (fibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
        { hom := f :
          InducedCategory.Hom (C :=
            ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
            CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })
⊢ ∀
    (f :
      Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (trivialCofibrations (Plus.{u_2, u_1} C)) (fibrations (Plus.{u_2, u_1} C))
        f)

Tactic:
⟨f⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
⊢ min (n - 1) m + 1 ≤ n

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
⊢ min (n - 1) m ≤ m

Tactic:
simp