awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : weakEquivalences (HoCat.{v, u} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f)
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution (CategoryTheory.Functor.map toHoCat f))
have hf₁ : WeakEquivalence f
Tactic: rw [← weakEquivalence_iff, weakEquivalence_toHoCat_map_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X))
    (CategoryTheory.Functor.map HoCat.bifibrantResolution (CategoryTheory.Functor.map toHoCat f))
have rw : IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X)) (Y :=
  Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat Y))
  (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f) :
    Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶
      Functor.obj BifibrantObject.toHoCat Y.bifibrantResolutionObj)
Tactic: rw [HoCat.bifibrantResolution_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (X := Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat X)) (Y :=
    Functor.obj HoCat.bifibrantResolution (Functor.obj toHoCat Y))
    (CategoryTheory.Functor.map BifibrantObject.toHoCat (bifibrantResolutionMap f) :
      Functor.obj BifibrantObject.toHoCat X.bifibrantResolutionObj ⟶
        Functor.obj BifibrantObject.toHoCat Y.bifibrantResolutionObj)
have x : weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
Tactic: apply Localization.inverts _ (weakEquivalences _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : CofibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject.{v, u} C) (bifibrantResolutionMap f)
have x : WeakEquivalence (bifibrantResolutionMap f)
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X : HoCat.{v, u} C
⊢ weakEquivalences (HoCat.{v, u} C) (NatTrans.app (Adjunction.unit HoCat.adj) X)
have rw : WeakEquivalence (NatTrans.app (Adjunction.unit HoCat.adj) X)
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ cofibrations C (coprod.inl ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have rw : Cofibration (coprod.inl ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: rw [← cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ trivialFibrations C (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have rw : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ∧
  WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: rw [mem_trivialFibrations_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ∧
    WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have left : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : CofibrantBrownFactorization f
inst_2 : IsCofibrant.{v_1, u_1} X
inst_3 : IsCofibrant.{v_1, u_1} Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v_1, u_1} X Y) (coprod.desc f (𝟙 Y))
left : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ∧
    WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have right : WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ trivialCofibrations C (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
have rw : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) ∧
  WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: rw [mem_trivialCofibrations_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) ∧
    WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
have left : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
left : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) ∧
    WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
have right : WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BrownLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : FibrantBrownFactorization f
inst_2 : IsFibrant.{v_1, u_1} X
inst_3 : IsFibrant.{v_1, u_1} Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v_1, u_1} Y X) (prod.lift f (𝟙 X))
⊢ fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst)
have rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst)
Tactic: rw [← fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f
have rw : trivialFibrations C f ↔ fibrations C f ∧ weakEquivalences C f
Tactic: rw [fibration_iff, weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : CategoryWithWeakEquivalences.{v, u} C
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f
have rw : trivialCofibrations C f ↔ cofibrations C f ∧ weakEquivalences C f
Tactic: rw [cofibration_iff, weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence f.hom
have simp : weakEquivalences P.FullSubcategory f ↔ weakEquivalences C f.hom
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_2 : WeakEquivalence f
⊢ WeakEquivalence (P.ι.map f)
have dsimp : WeakEquivalence f.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
f g : X ⟶ Y
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₂ : Relation.EqvGen (homRel C) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
inst_2 : IsFibrant.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
rw₂ : Relation.EqvGen (homRel C) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₃ : (fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isFibrant_tgt.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (CofibrantObject.{v_1, u_1} C) f ↔ weakEquivalences (CofibrantObject.{v_1, u_1} C) g
have simp : WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Tactic: simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom
have obtain : ∀ (P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))) (h : P.RightHomotopy f.hom g.hom),
  WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f : X ⟶ Y
⊢ WeakEquivalence (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔ WeakEquivalence f
have simp : weakEquivalences (HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔
  weakEquivalences (CofibrantObject.{v_1, u_1} C) f
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : CofibrantObject.{v_1, u_1} C
x_2 : x ⟶ x_1
h : weakEquivalences (CofibrantObject.{v_1, u_1} C) x_2
⊢ MorphismProperty.inverseImage (weakEquivalences (HoCat.{v_1, u_1} C)) toHoCat x_2
have h₁ : WeakEquivalence x_2
Tactic: simp only [← weakEquivalence_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g
have obtain : ∀ (P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))),
  P.IsVeryGood →
    ∀ (h : P.RightHomotopy f.hom g.hom),
      AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject.{v_1, u_1} C)) f g
have rw : L.map f = L.map g
Tactic: rw [areEqualizedByLocalization_iff L]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ L.map f = L.map g
have suffices : Eq (α := L.obj (mk P.P) ⟶ L.obj (mk (Y.obj (P := cofibrantObjects C)))) (L.map (homMk P.p₀)) (L.map (homMk P.p₁))
Tactic: suffices L.map (homMk P.p₀) = L.map (homMk P.p₁) by
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp, this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ weakEquivalences (CofibrantObject.{v_1, u_1} C) (X := mk (Y.obj (P := cofibrantObjects C))) (Y := mk P.P) (homMk P.ι)
have simp : WeakEquivalence P.ι
Tactic: simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : CofibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : PathObject.{v_1, u_1} (Y.obj (P := cofibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C)
    (weakEquivalences (CofibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (CofibrantObject.{v_1, u_1} C))
⊢ Eq (α := L.obj (mk P.P) ⟶ L.obj (mk (Y.obj (P := cofibrantObjects C)))) (L.map (homMk P.p₀)) (L.map (homMk P.p₁))
have this : IsIso (X := L.obj (mk (Y.obj (P := cofibrantObjects C)))) (Y := L.obj (mk P.P)) (L.map (homMk P.ι))
Tactic: have := Localization.inverts L (weakEquivalences _) (homMk P.ι) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences (HoCat.{v_1, u_1} C)) (toHoCatLocalizerMorphism C)
have apply : Eq (α := MorphismProperty.{v_1, u_1} (CofibrantObject.{v_1, u_1} C)) (weakEquivalences (CofibrantObject.{v_1, u_1} C))
  (MorphismProperty.inverseImage (D :=
    CategoryTheory.Quotient.{v_1, u_1} (C := CofibrantObject.{v_1, u_1} C) (homRel C))
    (weakEquivalences (HoCat.{v_1, u_1} C)) (Quotient.functor (homRel C)))
Tactic: apply (factorsThroughLocalization C).isLocalizedEquivalence
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p
have have : ∀
  (h :
    MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
      (initial.to X)),
  ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p
Tactic: have h := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C)
    (initial.to X)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
⊢ ∃ (X' : C) (_ : IsCofibrant.{v_1, u_1} X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p
have refine : IsCofibrant.{v_1, u_1} (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: refine ⟨h.Z, ?_, h.p, inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
h :
  MorphismProperty.MapFactorizationData.{v_1, u_1} (cofibrations C) (trivialFibrations C) (X := initial.{v_1, u_1} C)
    (initial.to X)
⊢ IsCofibrant.{v_1, u_1} (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have rw : Cofibration (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: rw [isCofibrant_iff_of_isInitial h.i initialIsInitial]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ ∃ (g : resolutionObj.{v_1, u_1} X ⟶ resolutionObj.{v_1, u_1} Y), g ≫ pResolutionObj Y = pResolutionObj X ≫ f
have sq : CommSq (W := initial.{v_1, u_1} C) (initial.to (resolutionObj.{v_1, u_1} Y)) (initial.to (resolutionObj.{v_1, u_1} X))
  (pResolutionObj Y) (pResolutionObj X ≫ f)
Tactic: have sq : CommSq (initial.to _) (initial.to _) (pResolutionObj Y)
    (pResolutionObj X ≫ f) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f
have rw : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f ≫ pResolutionObj Y) ↔ WeakEquivalence f
Tactic: rw [← weakEquivalence_postcomp_iff _ (pResolutionObj Y),
    HoCat.resolutionMap_fac, weakEquivalence_precomp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
rw : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f ≫ pResolutionObj Y) ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f
have rw₁ : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (pResolutionObj X ≫ f) ↔ WeakEquivalence f
Tactic: rw [← weakEquivalence_postcomp_iff _ (pResolutionObj Y),
    HoCat.resolutionMap_fac, weakEquivalence_precomp_iff]