awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f :
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, u_2} C c) (CategoryTheory.Quotient.mk (r := homotopic C c) K)
    (CategoryTheory.Quotient.mk (r := homotopic C c) L)
⊢ quasiIso C c f ↔ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) f
have h : ∀ (f : K ⟶ L),
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) ↔
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
Tactic: obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) ↔
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
have h : quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) →
  MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) →
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) ↔
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
have h₁ : MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) →
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
hf :
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
have hf₁ : HomologicalComplex.quasiIso C c f
Tactic: rw [quotient_map_mem_quasiIso_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
K' L' : HomologicalComplex.{v_1, u_1, u_2} C c
g : K' ⟶ L'
h : HomologicalComplex.quasiIso C c g
e :
  Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
    Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
have h₁ : ∀ (h : quasiIso C c (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g))
  (e :
    Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
      Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
        CategoryTheory.Quotient.mk (r := homotopic C c) L)
        (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)),
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
Tactic: rw [← quotient_map_mem_quasiIso_iff] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f g : K ⟶ L
⊢ homotopic C c f g →
    Eq.{u_3 + 1} (α :=
      Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
      (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)
have this : ∀ (h : Homotopy f g),
  Eq.{u_3 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
    (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ :
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, u_2} C c) (CategoryTheory.Quotient.mk (r := homotopic C c) K)
    (CategoryTheory.Quotient.mk (r := homotopic C c) L)
⊢ HomotopyCategory.quasiIso C c φ →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (CategoryTheory.Functor.map Qh φ)
have obtain : ∀ (φ : K ⟶ L),
  HomotopyCategory.quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ :
        Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))
Tactic: obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ HomotopyCategory.quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ :
        Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))
have rw : IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q φ) →
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
    Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
    Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
      Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
        (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
        (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))
Tactic: rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ,
    ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
⊢ homotopic C c f g → F.map f = F.map g
have this : ∀ (h : Homotopy f g), F.map f = F.map g
Tactic: ⟨h⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
⊢ F.map f = F.map g
have have : ∀ (this : DecidableRel c.Rel), F.map f = F.map g
Tactic: have : DecidableRel c.Rel := by classical infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
⊢ Functor.IsLocalization (C := HomologicalComplex.{v_1, u_2, u_1} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)
have h₁ : Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
  (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.{v_1, u_2, u_1} C c)
Tactic: apply Functor.IsLocalization.mk'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Localization (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
h₁ :
  Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.{v_1, u_2, u_1} C c)
⊢ Functor.IsLocalization (C := HomologicalComplex.{v_1, u_2, u_1} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)
have h₂ : Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
  (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
  (MorphismProperty.Localization (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomologicalComplex.homotopyEquivalences C c))
Tactic: apply Functor.IsLocalization.mk'
-- 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
X : Plus.{u_2, u_1} C
⊢ IsFibrant X ↔ ∀ (n : ℤ), Injective.{u_2, u_1} (X.obj (P := CochainComplex.plus C).X n)
have hL : IsZero (C := CochainComplex.{u_2, u_1, 0} C ℤ)
  (ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C) (⊤_ Plus.{u_2, u_1} C))
Tactic: rw [HomotopicalAlgebra.isFibrant_iff, fibration_iff,
    degreewiseEpiWithInjectiveKernel_iff_of_isZero]
-- 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 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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨A, hA⟩ := A
Cleared hypotheses: A, i, inst_2, hip, 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
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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨B, hB⟩ := B
Cleared hypotheses: B, b, i, inst_3, 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
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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨X, hX⟩ := X
Cleared hypotheses: X, p, inst_2, t, 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
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
⊢ sq.HasLift
have 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
Tactic: obtain ⟨Y, hY⟩ := Y
Cleared hypotheses: Y, b, p, inst_3, hip, 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
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
⊢ sq.HasLift
have hi : Mono i.hom
Tactic: have hi : Mono i.hom := inferInstance
-- 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
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
⊢ sq.HasLift
have hp : degreewiseEpiWithInjectiveKernel p.hom
Tactic: have hp : degreewiseEpiWithInjectiveKernel p.hom :=
      (fibration_iff p).1 inferInstance