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
b :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY
i :
  (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA).obj (P := CochainComplex.plus C) ⟶
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB).obj (P := CochainComplex.plus C)
inst_2 : Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i).hom
p :
  (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX).obj (P := CochainComplex.plus C) ⟶
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY).obj (P := CochainComplex.plus C)
inst_3 : Fibration (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel (ObjectProperty.homMk (P := CochainComplex.plus C) p).hom
hip :
  WeakEquivalence (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t :
  (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA).obj (P := CochainComplex.plus C) ⟶
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX).obj (P := CochainComplex.plus C)
sq :
  CommSq (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) b
obtain :
  ∀
    (b :
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB).obj (P := CochainComplex.plus C) ⟶
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY).obj (P := CochainComplex.plus C))
    (sq :
      CommSq (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.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨b, rfl⟩ := ObjectProperty.homMk_surjective b

Premises used: CategoryTheory.ObjectProperty.homMk_surjective, rfl
-- 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 :
  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)
⊢ QuasiIso i ∨ QuasiIso p

Tactic:
simpa only [weakEquivalence_iff] using hip

Premises used: CochainComplex.Plus.modelCategoryQuillen.weakEquivalence_iff
-- 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 :
  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)
⊢ QuasiIso i ∨ QuasiIso p

Tactic:
have hip : QuasiIso i ∨ QuasiIso p := by
      simpa only [weakEquivalence_iff] using hip
-- 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 :
  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
⊢ CommSq t i p b

Tactic:
replace sq : CommSq t i p b := sq.map (ObjectProperty.ι _)
-- 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
suffices : sq.HasLift
⊢ sq_1.HasLift

Tactic:
suffices sq.HasLift from ⟨⟨{ l := ObjectProperty.homMk sq.lift }⟩⟩
-- 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
⊢ ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)

Tactic:
have sq' (n : ℤ) : CommSq (t.f n) (i.f n) (p.f n) (b.f n) :=
      (sq.map (HomologicalComplex.eval _ _ n))
-- 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)
n : ℤ
⊢ HasLiftingProperty (i.f n) (p.f n)

Tactic:
have := (hp n).hasLiftingProperty (i.f n)
-- 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)
n : ℤ
this : HasLiftingProperty (i.f n) (p.f n)
⊢ ⋯.HasLift

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_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)
⊢ ∀ (n : ℤ), ⋯.HasLift

Tactic:
have (n : ℤ) : (sq' n).HasLift := by
      have := (hp n).hasLiftingProperty (i.f n)
      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_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
⊢ Eq (α := A ⟶ cokernel i) (i ≫ cokernel.π i) 0

Tactic:
simp