awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : AddRightCancelSemigroup ι
inst_3 : One ι
inst_4 : HasBinaryBiproducts.{v_1, u_1} C
inst_5 : CategoryWithHomology.{v_1, u_1} C
⊢ ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} (ComplexShape.down ι) C

Tactic:
(ComplexShape.down ι).QFactorsThroughHomotopy_of_exists_prev (fun _ => ⟨_, rfl⟩) C

Premises used: HAdd.hAdd, ComplexShape.QFactorsThroughHomotopy_of_exists_prev, Exists.intro, ComplexShape.down, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : AddRightCancelSemigroup ι
inst_3 : One ι
inst_4 : HasBinaryBiproducts.{v_1, u_1} C
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C (ComplexShape.down ι))
    (HomologicalComplex.quasiIso C (ComplexShape.down ι))
⊢ Functor.IsLocalization (C := HomotopyCategory.{v_1, u_1, u_2} C (ComplexShape.down ι)) (D :=
    HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C (ComplexShape.down ι)) HomologicalComplexUpToQuasiIso.Qh
    (HomotopyCategory.quasiIso C (ComplexShape.down ι))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
inst_3 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
inst_3 : CategoryWithHomology.{v_1, u_1} C
inst_4 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ))
    (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
⊢ Functor.IsLocalization (C := HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (D :=
    HomologicalComplexUpToQuasiIso.{v_1, u_1, 0, u_3} C (ComplexShape.up ℤ)) HomologicalComplexUpToQuasiIso.Qh
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : CategoryWithHomology.{v_2, u_2} D
inst_6 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_2, u_2, u_3} D c) (HomologicalComplex.quasiIso D c)
inst_7 : F.Additive
inst_8 : F.PreservesHomology
⊢ MorphismProperty.IsInvertedBy (C := HomologicalComplex.{v_1, u_1, u_3} C c) (D :=
    HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c) (HomologicalComplex.quasiIso C c)
    (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q)

Tactic:
apply (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).inverts

Premises used: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism, CategoryTheory.LocalizerMorphism.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : CategoryWithHomology.{v_2, u_2} D
inst_6 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_2, u_2, u_3} D c) (HomologicalComplex.quasiIso D c)
inst_7 : F.Additive
inst_8 : F.PreservesHomology
inst_9 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_3} C c) (HomologicalComplex.quasiIso C c)
inst_10 : ComplexShape.QFactorsThroughHomotopy.{u_3, v_1, u_1} c C
inst_11 : ComplexShape.QFactorsThroughHomotopy.{u_3, v_2, u_2} c D
inst_12 :
  IsLocalization (C := HomologicalComplex.{v_1, u_1, u_3} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex.{v_1, u_1, u_3} C c
⊢ Eq.{u_4 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_2, u_2, u_3, u_4} D c)
      (obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_3, u_5} C c) (F.mapHomologicalComplexUpToQuasiIso c)
        (obj HomologicalComplexUpToQuasiIso.Qh (obj (HomotopyCategory.quotient C c) K)))
      (obj HomologicalComplexUpToQuasiIso.Qh (obj (F.mapHomotopyCategory c) (obj (HomotopyCategory.quotient C c) K))))
    (NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)) K)
    (map (F.mapHomologicalComplexUpToQuasiIso c)
        (𝟙 (obj HomologicalComplexUpToQuasiIso.Qh (obj (HomotopyCategory.quotient C c) K))) ≫
      NatTrans.app (Iso.hom (F.mapHomologicalComplexUpToQuasiIsoFactors c)) K ≫
        𝟙
            (obj HomologicalComplexUpToQuasiIso.Qh
              (obj (F.mapHomotopyCategory c) (obj (HomotopyCategory.quotient C c) K))) ≫
          map HomologicalComplexUpToQuasiIso.Qh
            (𝟙 (obj (F.mapHomotopyCategory c) (obj (HomotopyCategory.quotient C c) K))))

Tactic:
simp only [map_id, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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
⊢ MorphismProperty.HasTwoOutOfThreeProperty (C := Plus.{u_2, u_1} C) (weakEquivalences (Plus.{u_2, u_1} C))

Tactic:
inferInstanceAs (quasiIso C).HasTwoOutOfThreeProperty

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.instHasTwoOutOfThreePropertyWeakEquivalences._proof_1
-- 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
⊢ MorphismProperty.IsStableUnderRetracts (C := Plus.{u_2, u_1} C) (weakEquivalences (Plus.{u_2, u_1} C))

Tactic:
inferInstanceAs (quasiIso C).IsStableUnderRetracts

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsWeakEquivalences._proof_1
-- 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
⊢ MorphismProperty.IsStableUnderRetracts (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))

Tactic:
inferInstanceAs (MorphismProperty.monomorphisms _).IsStableUnderRetracts

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsCofibrations._proof_1
-- 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
⊢ MorphismProperty.IsStableUnderRetracts (C := Plus.{u_2, u_1} C) (fibrations (Plus.{u_2, u_1} C))

Tactic:
inferInstanceAs (degreewiseEpiWithInjectiveKernel.inverseImage (ι C)).IsStableUnderRetracts

Premises used: _private.0.CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsFibrations._proof_1
-- 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
X Y : Plus.{u_2, u_1} C
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f

Tactic:
HomotopicalAlgebra.cofibration_iff _

Premises used: HomotopicalAlgebra.cofibrations, HomotopicalAlgebra.cofibration_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
X Y : Plus.{u_2, u_1} C
f : X ⟶ Y
⊢ Fibration f ↔ degreewiseEpiWithInjectiveKernel f.hom

Tactic:
HomotopicalAlgebra.fibration_iff _

Premises used: HomotopicalAlgebra.fibrations, HomotopicalAlgebra.fibration_iff, CategoryTheory.MorphismProperty.inverseImage, CochainComplex.degreewiseEpiWithInjectiveKernel
-- 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
X : Plus.{u_2, u_1} C
hL :
  IsZero (C := CochainComplex.{u_2, u_1, 0} C ℤ)
    (ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C) (⊤_ Plus.{u_2, u_1} C))
⊢ IsFibrant X ↔ ∀ (n : ℤ), Injective.{u_2, u_1} (X.obj (P := CochainComplex.plus C).X n)

Tactic:
rw [HomotopicalAlgebra.isFibrant_iff, fibration_iff,
    degreewiseEpiWithInjectiveKernel_iff_of_isZero]

Premises used: CochainComplex.degreewiseEpiWithInjectiveKernel_iff_of_isZero, CochainComplex.Plus.modelCategoryQuillen.fibration_iff, HomotopicalAlgebra.isFibrant_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
X : Plus.{u_2, u_1} C
⊢ IsZero (C := CochainComplex.{u_2, u_1, 0} C ℤ)
    (ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C) (⊤_ Plus.{u_2, u_1} C))

Tactic:
Functor.map_isZero (Plus.ι C) (IsZero.of_mono_zero _ X)

Premises used: CochainComplex.Plus.ι, CategoryTheory.Limits.IsZero.of_mono_zero, CategoryTheory.Functor.map_isZero
-- 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
X : Plus.{u_2, u_1} C
⊢ IsZero (C := CochainComplex.{u_2, u_1, 0} C ℤ)
    (ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C) (⊤_ Plus.{u_2, u_1} C))

Tactic:
exact Functor.map_isZero (Plus.ι C) (IsZero.of_mono_zero _ X)

Premises used: CochainComplex.Plus.ι, CategoryTheory.Limits.IsZero.of_mono_zero, CategoryTheory.Functor.map_isZero
-- 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
X Y : Plus.{u_2, u_1} C
f : X ⟶ Y
⊢ WeakEquivalence f ↔ QuasiIso f.hom

Tactic:
HomotopicalAlgebra.weakEquivalence_iff _

Premises used: CochainComplex.Plus.quasiIso, HomologicalComplex.quasiIso, CategoryTheory.MorphismProperty.inverseImage, HomotopicalAlgebra.weakEquivalence_iff, HomotopicalAlgebra.weakEquivalences
-- 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 : Plus.{u_2, u_1} C
i : A ⟶ B
inst_2 rwa rwa₁ rwa₂ rwa₃ : Cofibration i
⊢ Mono i

Tactic:
rwa [← cofibration_iff]

Premises used: CochainComplex.Plus.modelCategoryQuillen.cofibration_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 B X Y : Plus.{u_2, u_1} C
i : A ⟶ B
p : X ⟶ Y
inst_2 : Mono i
inst_3 : Fibration p
hip : WeakEquivalence i ∨ WeakEquivalence p
t : A ⟶ X
b : B ⟶ Y
sq : CommSq t i p b
obtain :
  ∀ (A : CochainComplex.{u_2, u_1, 0} C ℤ) (hA : CochainComplex.plus C A)
    (i : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶ B) [Mono i]
    (hip : WeakEquivalence i ∨ WeakEquivalence p)
    {t : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶ X} (sq : CommSq t i p b), sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨A, hA⟩ := A
-- 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
B X Y : Plus.{u_2, u_1} C
p : X ⟶ Y
inst_2 : Fibration p
b : B ⟶ Y
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
i : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶ B
inst_3 : Mono i
hip : WeakEquivalence i ∨ WeakEquivalence p
t : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶ X
sq : CommSq t i p b
obtain :
  ∀ (B : CochainComplex.{u_2, u_1, 0} C ℤ) (hB : CochainComplex.plus C B)
    {b : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB ⟶ Y}
    (i :
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    [Mono i] (hip : WeakEquivalence i ∨ WeakEquivalence p) (sq : CommSq t i p b), sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨B, hB⟩ := B
-- 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
X Y : Plus.{u_2, u_1} C
p : X ⟶ Y
inst_2 : Fibration p
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
t : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶ X
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
b : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB ⟶ Y
i :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB
inst_3 : Mono i
hip : WeakEquivalence i ∨ WeakEquivalence p
sq : CommSq t i p b
obtain :
  ∀ (X : CochainComplex.{u_2, u_1, 0} C ℤ) (hX : CochainComplex.plus C X)
    (p : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX ⟶ Y) [Fibration p]
    {t :
      ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX}
    (hip : WeakEquivalence i ∨ WeakEquivalence p) (sq : CommSq t i p b), sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨X, hX⟩ := 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
Y : Plus.{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
b : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB ⟶ Y
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
p : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX ⟶ Y
inst_3 : Fibration p
t :
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA ⟶
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX
hip : WeakEquivalence i ∨ WeakEquivalence p
sq : CommSq t i p b
obtain :
  ∀ (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)
    [Fibration p] (hip : WeakEquivalence i ∨ WeakEquivalence p) (sq : CommSq t i p b), sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨Y, hY⟩ := Y
-- 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
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
⊢ Mono i.hom

Tactic:
have hi : Mono i.hom := inferInstance
-- 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
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
⊢ degreewiseEpiWithInjectiveKernel p.hom

Tactic:
have hp : degreewiseEpiWithInjectiveKernel p.hom :=
      (fibration_iff p).1 inferInstance
-- 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
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
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
⊢ sq.HasLift

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

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
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
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
⊢ sq.HasLift

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

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
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
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
⊢ sq.HasLift

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

Premises used: CategoryTheory.ObjectProperty.homMk_surjective, rfl