awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences (HoCat.{v_1, u_1} C)) (toHoCatLocalizerMorphism C)
have apply : Eq (α := MorphismProperty.{v_1, u_1} (FibrantObject.{v_1, u_1} C)) (weakEquivalences (FibrantObject.{v_1, u_1} C))
  (MorphismProperty.inverseImage (D := CategoryTheory.Quotient.{v_1, u_1} (C := FibrantObject.{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.FibrantObjectHomotopy (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) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i
have have : ∀
  (h :
    MorphismProperty.MapFactorizationData.{v_1, u_1} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
      (terminal.from X)),
  ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i
Tactic: have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from X)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
⊢ ∃ (X' : C) (_ : IsFibrant.{v_1, u_1} X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i
have refine : IsFibrant.{v_1, u_1} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: refine ⟨h.Z, ?_, h.i, inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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} (trivialCofibrations C) (fibrations C) (Y := terminal.{v_1, u_1} C)
    (terminal.from X)
⊢ IsFibrant.{v_1, u_1} (h.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C))
have rw : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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), iResolutionObj X ≫ g = f ≫ iResolutionObj Y
have sq : CommSq (Z := terminal.{v_1, u_1} C) (f ≫ iResolutionObj Y) (iResolutionObj X)
  (terminal.from (resolutionObj.{v_1, u_1} Y)) (terminal.from (resolutionObj.{v_1, u_1} X))
Tactic: have sq : CommSq (f ≫ iResolutionObj Y) (iResolutionObj X)
    (terminal.from _) (terminal.from _) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 (Y := resolutionObj.{v_1, u_1} Y) (iResolutionObj X ≫ resolutionMap f) ↔ WeakEquivalence f
Tactic: rw [← weakEquivalence_precomp_iff (iResolutionObj X),
    HoCat.resolutionMap_fac, weakEquivalence_postcomp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 (Y := resolutionObj.{v_1, u_1} Y) (iResolutionObj X ≫ resolutionMap f) ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f
have rw₁ : WeakEquivalence (Y := resolutionObj.{v_1, u_1} Y) (f ≫ iResolutionObj Y) ↔ WeakEquivalence f
Tactic: rw [← weakEquivalence_precomp_iff (iResolutionObj X),
    HoCat.resolutionMap_fac, weakEquivalence_postcomp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 (Y := resolutionObj.{v_1, u_1} Y) (iResolutionObj X ≫ resolutionMap f) ↔ WeakEquivalence f
rw₁ : WeakEquivalence (Y := resolutionObj.{v_1, u_1} Y) (f ≫ iResolutionObj Y) ↔ WeakEquivalence f
⊢ WeakEquivalence (X := resolutionObj.{v_1, u_1} X) (resolutionMap f) ↔ WeakEquivalence f
have rw₂ : WeakEquivalence f ↔ WeakEquivalence f
Tactic: rw [← weakEquivalence_precomp_iff (iResolutionObj X),
    HoCat.resolutionMap_fac, weakEquivalence_postcomp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ Eq (α :=
    Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj toHoCat (mk (resolutionObj.{v_1, u_1} X)))
      (Functor.obj toHoCat (mk Y)))
    (CategoryTheory.Functor.map toHoCat (homMk f)) (CategoryTheory.Functor.map toHoCat (homMk g))
have h₁ : homRel C (X := mk (resolutionObj.{v_1, u_1} X)) (Y := mk Y) (homMk f) (homMk g)
Tactic: apply toHoCat_map_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ LeftHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
    (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
    (InducedCategory.Hom.hom (homMk g))
have h₁ : RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
  (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
  (InducedCategory.Hom.hom (homMk g))
Tactic: apply RightHomotopyRel.leftHomotopyRel
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : C
inst_2 : IsFibrant.{v_1, u_1} Y
f g : resolutionObj.{v_1, u_1} X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ RightHomotopyRel (X := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
    (Y := ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)) (InducedCategory.Hom.hom (homMk f))
    (InducedCategory.Hom.hom (homMk g))
have h₁ : ∀
  (h :
    Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk (iResolutionObj X ≫ f))
      (RightHomotopyClass.mk (iResolutionObj X ≫ g))),
  Eq (α :=
    RightHomotopyClass (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk (resolutionObj.{v_1, u_1} X)))
      (ObjectProperty.FullSubcategory.obj (P := fibrantObjects C) (mk Y)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk f)))
    (RightHomotopyClass.mk (InducedCategory.Hom.hom (homMk g)))
Tactic: rw [← RightHomotopyClass.mk_eq_mk_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α := x ⟶ mk (resolutionObj.{v_1, u_1} (Functor.obj ι x_1))) (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) })
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
      { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f))))
have h : Eq (α :=
  (Functor.obj toHoCat x).as (r := homRel C).obj (P := fibrantObjects C) ⟶
    ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
      (Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x_1)))
  (InducedCategory.Hom.hom (f ≫ { hom := iResolutionObj (Functor.obj ι x_1) }))
  (InducedCategory.Hom.hom
    (CategoryStruct.comp (Y := Quotient.as (r := homRel C) (Functor.obj (ι ⋙ resolution) x))
      { hom := iResolutionObj (Functor.obj ι x) } (homMk (resolutionMap (CategoryTheory.Functor.map ι f)))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{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 toHoCat X) (Y :=
  Functor.obj HoCat.resolution (X.obj (P := fibrantObjects C)))
  (CategoryTheory.Functor.map toHoCat { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{v_1, u_1} C
⊢ WeakEquivalence.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (Y :=
    Functor.obj HoCat.resolution (X.obj (P := fibrantObjects C)))
    (CategoryTheory.Functor.map toHoCat { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })
have rw : WeakEquivalence.{v_1, u_1} (C := C) (X := X.obj (P := fibrantObjects C)) (Y :=
  ObjectProperty.FullSubcategory.obj (P := fibrantObjects C)
    (mk (HoCat.resolutionObj.{v_1, u_1} (X.obj (P := fibrantObjects C)))))
  (InducedCategory.Hom.hom { hom := HoCat.iResolutionObj (X.obj (P := fibrantObjects C)) })
Tactic: rw [weakEquivalence_toHoCat_map_iff, weakEquivalence_iff_of_objectProperty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 : FibrantObject.{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.FibrantObjectHomotopy (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 : FibrantObject.{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.FibrantObjectHomotopy (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 : FibrantObject.{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.FibrantObjectHomotopy (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 (Y := Functor.comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (HoCat.resolutionCompToLocalizationNatTrans L)
have rw : ∀ (X : C),
  IsIso (Y := (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.FibrantObjectHomotopy (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 (Y := (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 (Y :=
  Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
    (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
  (HoCat.iResolutionObj X)
Tactic: apply Localization.inverts L (weakEquivalences _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (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 (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
      (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
    (HoCat.iResolutionObj X)
have x : WeakEquivalence.{v_1, u_1} (Y :=
  Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) ι
    (Quotient.as (r := homRel C) (Functor.obj HoCat.resolution X)))
  (HoCat.iResolutionObj X)
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ G
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{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 (FibrantObject.{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.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ 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 (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
have have : ∀
  (this :
    Localization.Lifting Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)),
  LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)
Tactic: have : Localization.Lifting Lfib (weakEquivalences (FibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hfib : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lfibπ : HoCat.{v_1, u_1} C ⥤ Hfib := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lfib : FibrantObject.{v_1, u_1} C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hfib ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lfibπ F)
G : H ⥤ Hfib :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lfibπ
eG : HoCat.resolution ⋙ Lfibπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lfibπ 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 Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lfibπ) (F ⋙ G)
E : Hfib ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lfib (weakEquivalences (FibrantObject.{v_1, u_1} C)) Lfib (ι ⋙ HoCat.resolution ⋙ Lfibπ)
      (𝟭 Hfib) (F ⋙ G)
      (asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lfibπ) ≪≫ associator ι HoCat.resolution Lfibπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (Iso.symm (asIso (HoCat.resolutionCompToLocalizationNatTrans L))))
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{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.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : FibrantObject.{v_1, u_1} C
⊢ IsFibrant.{v_1, u_1}
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      X)
have dsimp : IsFibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
⊢ Eq (α := LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (leftHomotopyClassToHom L)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y))
have h : ∀ (f : LeftHomotopyClass X Y),
  leftHomotopyClassToHom L f =
    Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
H : Type u_2
inst_2 : Category.{v_2, u_2} H
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C H
inst_3 : L.IsLocalization (weakEquivalences C)
X Y : C
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
f : LeftHomotopyClass X Y
⊢ leftHomotopyClassToHom L f =
    Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y) f
have h : ∀ (f : X ⟶ Y),
  leftHomotopyClassToHom L (LeftHomotopyClass.mk f) =
    Function.comp (α := LeftHomotopyClass X Y) (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y)
      (LeftHomotopyClass.mk f)
Tactic: obtain ⟨f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f