awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₁ : WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (pResolutionObj X ≫ f) ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f
have rw₂ : WeakEquivalence f ↔ 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 : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ Eq (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk X))
      (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} Y))))
    (CategoryTheory.Functor.map toHoCat (homMk f)) (CategoryTheory.Functor.map toHoCat (homMk g))
have h₁ : homRel C (X := mk X) (Y := mk (resolutionObj.{v_1, u_1} Y)) (homMk f) (homMk g)
Tactic: apply toHoCat_map_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 : C
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
    (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))
have h₁ : LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
  ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
  (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))
Tactic: apply LeftHomotopyRel.rightHomotopyRel
-- 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
inst_2 : IsCofibrant.{v_1, u_1} X
Y : C
f g : X ⟶ resolutionObj.{v_1, u_1} Y
h : LeftHomotopyRel (f ≫ pResolutionObj Y) (g ≫ pResolutionObj Y)
⊢ LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X)) (Y :=
    ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y)))
    (InducedCategory.Hom.hom (homMk f)) (InducedCategory.Hom.hom (homMk g))
have h₁ : ∀
  (h :
    Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk (f ≫ pResolutionObj Y))
      (LeftHomotopyClass.mk (g ≫ pResolutionObj Y))),
  Eq (α :=
    LeftHomotopyClass (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk X))
      (ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C) (mk (resolutionObj.{v_1, u_1} Y))))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (LeftHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))
Tactic: rw [← LeftHomotopyClass.mk_eq_mk_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 x_1 : CofibrantObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α := mk (resolutionObj.{v_1, u_1} (Functor.obj ι x)) ⟶ x_1)
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1))
      (homMk (resolutionMap (CategoryTheory.Functor.map ι f))) { hom := pResolutionObj (Functor.obj ι x_1) })
    ({ hom := pResolutionObj (Functor.obj ι x) } ≫ f)
have h : Eq (α :=
  ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
      (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x)) ⟶
    (Functor.obj toHoCat x_1).as (r := homRel C).obj (P := cofibrantObjects C))
  (InducedCategory.Hom.hom
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1))
      (homMk (resolutionMap (CategoryTheory.Functor.map ι f))) { hom := pResolutionObj (Functor.obj ι x_1) }))
  (InducedCategory.Hom.hom ({ hom := pResolutionObj (Functor.obj ι x) } ≫ f))
Tactic: ext : 1
-- 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 : CofibrantObject.{v_1, u_1} C
⊢ WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)
have dsimp : WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X :=
  Functor.obj HoCat.resolution (X.obj (P := cofibrantObjects C))) (Y := Functor.obj toHoCat X)
  (CategoryTheory.Functor.map toHoCat { hom := HoCat.pResolutionObj (X.obj (P := cofibrantObjects C)) } :
    Functor.obj toHoCat (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := cofibrantObjects C)))) ⟶ Functor.obj toHoCat X)
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 : CofibrantObject.{v_1, u_1} C
⊢ WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X :=
    Functor.obj HoCat.resolution (X.obj (P := cofibrantObjects C))) (Y := Functor.obj toHoCat X)
    (CategoryTheory.Functor.map toHoCat { hom := HoCat.pResolutionObj (X.obj (P := cofibrantObjects C)) } :
      Functor.obj toHoCat (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := cofibrantObjects C)))) ⟶
        Functor.obj toHoCat X)
have rw : WeakEquivalence.{v_1, u_1} (C := C) (X :=
  ObjectProperty.FullSubcategory.obj (P := cofibrantObjects C)
    (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := cofibrantObjects C)))))
  (Y := X.obj (P := cofibrantObjects C))
  (InducedCategory.Hom.hom { hom := HoCat.pResolutionObj (X.obj (P := cofibrantObjects C)) })
Tactic: rw [weakEquivalence_toHoCat_map_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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)
have rw : ∀ (X : CofibrantObject.{v_1, u_1} C), IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
X : CofibrantObject.{v_1, u_1} C
⊢ IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)
have x : weakEquivalences (HoCat.{v_1, u_1} C) (NatTrans.app HoCat.ιCompResolutionNatTrans X)
Tactic: apply Localization.inverts L (weakEquivalences _)
-- 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (HoCat.{v_1, u_1} C) D
inst_3 : L.IsLocalization (weakEquivalences (HoCat.{v_1, u_1} C))
X : CofibrantObject.{v_1, u_1} C
⊢ weakEquivalences (HoCat.{v_1, u_1} C) (NatTrans.app HoCat.ιCompResolutionNatTrans X)
have x : WeakEquivalence (NatTrans.app HoCat.ιCompResolutionNatTrans X)
Tactic: rw [← weakEquivalence_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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
⊢ IsIso (X := Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (HoCat.resolutionCompToLocalizationNatTrans L)
have rw : ∀ (X : C),
  IsIso (X := (Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)).obj X)
    (NatTrans.app (HoCat.resolutionCompToLocalizationNatTrans L) X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
X : C
⊢ IsIso (X := (Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)).obj X)
    (NatTrans.app (HoCat.resolutionCompToLocalizationNatTrans L) X)
have x : weakEquivalences.{v_1, u_1} C (X :=
  Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
    (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
  (HoCat.pResolutionObj X)
Tactic: apply Localization.inverts L (weakEquivalences _)
-- 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
X : C
⊢ weakEquivalences.{v_1, u_1} C (X :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.pResolutionObj X)
have x : WeakEquivalence.{v_1, u_1} (X :=
  Functor.obj.{v_1, v_1, u_1, u_1} (C := CofibrantObject.{v_1, u_1} C) ι
    (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
  (HoCat.pResolutionObj X)
Tactic: rw [← weakEquivalence_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
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
have have : ∀
  (this :
    Localization.Lifting L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) (G ⋙ F)),
  LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
Tactic: have : Localization.Lifting L (weakEquivalences C)
      (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eG.symm _ ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eF'.symm⟩
-- 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
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
have have : ∀
  (this :
    Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)),
  LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
Tactic: have : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩
-- 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
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this_1 :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
this :
  Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
E : Hcof ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ)
      (𝟭 Hcof) (F ⋙ G)
      ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫ associator ι HoCat.resolution Lcofπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
have this₁ : F.IsEquivalence
Tactic: have : F.IsEquivalence := E.isEquivalence_functor
-- 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 : CofibrantObject.{v_1, u_1} C
⊢ IsCofibrant.{v_1, u_1}
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      X)
have dsimp : IsCofibrant.{v_1, u_1} (X.obj (P := cofibrantObjects C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
⊢ WeakEquivalence P.symm.π
have dsimp : WeakEquivalence P.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
⊢ Cofibration P.i₀
have rw : Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P.i)
Tactic: rw [← P.inl_i]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
⊢ Cofibration P.i₁
have rw : Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr P.i)
Tactic: rw [← P.inr_i]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
⊢ cofibrations C (X := coprod.{v, u} A A) P.i
have rw : Cofibration (X := coprod.{v, u} A A) P.i
Tactic: rw [← cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
⊢ Cofibration (X := coprod.{v, u} A A) P.symm.i
have hi : cofibrations C (X := coprod.{v, u} A A) P.i
Tactic: have hi : cofibrations C P.i := by rw [← cofibration_iff]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
⊢ Cofibration (X := coprod.{v, u} A A) P.symm.i
have rw : cofibrations C (X := coprod.{v, u} A A)
  (CategoryStruct.comp (Y := coprod.{v, u} A A) (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A)
      (P.i : coprod.{v, u} A A ⟶ P.I) :
    coprod.{v, u} A A ⟶ P.I)
Tactic: rw [P.symm_i, cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
⊢ cofibrations C (X := coprod.{v, u} A A)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I)
have refine : Arrow.mk (X := coprod.{v, u} A A)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I) ≅
  Arrow.mk (X := coprod.{v, u} A A) P.i
Tactic: refine ((cofibrations C).arrow_mk_iso_iff ?_).2 hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
inst_6 : HasBinaryCoproducts.{v, u} C
inst_7 : P.IsVeryGood
⊢ Fibration P.symm.π
have dsimp : Fibration P.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : Cylinder.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} A A)
    (codiag A)
⊢ Fibration (ofFactorizationData h).π
have dsimp : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))
have simp : WeakEquivalence.{v, u} (𝟙 A)
Tactic: simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π
have this : WeakEquivalence
  (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π sorry))
Tactic: have : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫
        pushout.desc P.π P'.π (by simp)) := by
      simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]
      infer_instance