awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB
inst_2 : Mono i
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
t :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX
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
p :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY
inst_3 : Fibration p
hip : WeakEquivalence i ∨ WeakEquivalence p
sq : CommSq t i p b
hi : Mono i.hom
hp : degreewiseEpiWithInjectiveKernel p.hom
⊢ sq.HasLift
have obtain : ∀
  (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))
  [Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i)]
  (hip : WeakEquivalence (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨ WeakEquivalence p)
  (sq : CommSq t (ObjectProperty.homMk (P := CochainComplex.plus C) i) p b)
  (hi : Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i).hom), sq.HasLift
Tactic: obtain ⟨i, rfl⟩ := ObjectProperty.homMk_surjective i
Cleared hypotheses: i, inst_2, hip, sq, hi
-- 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
t :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX
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
p :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY
inst_2 : Fibration p
hp : degreewiseEpiWithInjectiveKernel p.hom
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_3 : Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hip : WeakEquivalence (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨ WeakEquivalence p
sq : CommSq t (ObjectProperty.homMk (P := CochainComplex.plus C) i) p b
hi : Mono (ObjectProperty.homMk (P := CochainComplex.plus C) i).hom
⊢ sq.HasLift
have obtain : ∀
  (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))
  [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))
  (sq :
    CommSq t (ObjectProperty.homMk (P := CochainComplex.plus C) i) (ObjectProperty.homMk (P := CochainComplex.plus C) p)
      b),
  sq.HasLift
Tactic: obtain ⟨p, rfl⟩ := ObjectProperty.homMk_surjective p
Cleared hypotheses: p, inst_2, hp, hip, sq
-- 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
t :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX
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)
sq :
  CommSq t (ObjectProperty.homMk (P := CochainComplex.plus C) i) (ObjectProperty.homMk (P := CochainComplex.plus C) p) b
⊢ sq.HasLift
have obtain : ∀
  (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),
  sq.HasLift
Tactic: obtain ⟨t, rfl⟩ := ObjectProperty.homMk_surjective t
Cleared hypotheses: t, sq
-- 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
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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨b, rfl⟩ := ObjectProperty.homMk_surjective b
Cleared hypotheses: b, sq
-- 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 :
  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)
⊢ sq.HasLift
have hip₁ : QuasiIso i ∨ QuasiIso p
Tactic: have hip : QuasiIso i ∨ QuasiIso p := by
      simpa only [weakEquivalence_iff] using hip
-- 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 :
  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.HasLift
have sq₁ : CommSq t i p b
Tactic: replace sq : CommSq t i p b := sq.map (ObjectProperty.ι _)
-- 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_1.HasLift
have suffices : sq.HasLift
Tactic: suffices sq.HasLift from ⟨⟨{ l := ObjectProperty.homMk sq.lift }⟩⟩
-- 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.HasLift
have sq' : ∀ (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))
-- 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)
n : ℤ
⊢ ⋯.HasLift
have this : HasLiftingProperty (i.f n) (p.f n)
Tactic: have := (hp n).hasLiftingProperty (i.f n)
-- 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)
⊢ sq.HasLift
have this : ∀ (n : ℤ), sorry.HasLift
Tactic: have (n : ℤ) : (sq' n).HasLift := by
      have := (hp n).hasLiftingProperty (i.f n)
      infer_instance