awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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_2 :
  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))))
this : F.IsEquivalence
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lfib L F

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk', HomotopicalAlgebra.FibrantObject.localizerMorphism
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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_2 :
  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))))
this : F.IsEquivalence
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
exact LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lfib L F

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk', HomotopicalAlgebra.FibrantObject.localizerMorphism
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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
dsimp : IsFibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
⊢ IsFibrant.{v_1, u_1}
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      X)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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} (X.obj (P := fibrantObjects C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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)
⊢ Functor.IsLocalization (C := FibrantObject.{v_1, u_1} C) (ι ⋙ L) (weakEquivalences (FibrantObject.{v_1, u_1} C))

Tactic:
inferInstanceAs (((localizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
f : X ⟶ Y
⊢ leftHomotopyClassToHom L (LeftHomotopyClass.mk f) = L.map f

Tactic:
rfl

Premises used: HomotopicalAlgebra.leftHomotopyClassToHom, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
f : X ⟶ Y
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) = L.map f

Tactic:
rfl

Premises used: HomotopicalAlgebra.rightHomotopyClassToHom, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
h :
  ∀ (f : LeftHomotopyClass X Y),
    leftHomotopyClassToHom L f =
      Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
        (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y) f
⊢ 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))

Tactic:
ext f
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
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)
⊢ leftHomotopyClassToHom L f =
    Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (⇑leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y) f

Tactic:
obtain ⟨f, rfl⟩ := f.mk_surjective

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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 : 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:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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))

Tactic:
have : (leftHomotopyClassToHom L : LeftHomotopyClass X Y → _) =
      rightHomotopyClassToHom L ∘ leftHomotopyClassEquivRightHomotopyClass := by
    ext f
    obtain ⟨f, rfl⟩ := f.mk_surjective
    simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  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))
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) ↔
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
inr :
  ∀
    (this :
      ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
        Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
    ¬IsCofibrant.{v_1, u_1} Y → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
wlog :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y],
    IsCofibrant.{v_1, u_1} Y → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
wlog _ : IsCofibrant Y generalizing Y

Premises used: HomotopicalAlgebra.IsCofibrant
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
inr :
  ∀ (Y' : C),
    IsCofibrant.{v_1, u_1} Y' →
      ∀ (p : Y' ⟶ Y),
        Fibration p → WeakEquivalence p → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
obtain ⟨Y', _, p, _, _⟩ := CofibrantObject.HoCat.exists_resolution Y

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
⊢ IsFibrant.{v_1, u_1} Y'

Tactic:
have _ : IsFibrant Y' := isFibrant_of_fibration p
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
⊢ Function.Bijective (α := RightHomotopyClass X Y') (rightHomotopyClassToHom L)

Tactic:
have hY' := this Y' inferInstance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := RightHomotopyClass X Y') (rightHomotopyClassToHom L)
inr :
  ∀ (hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)),
    Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
simp only [← bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom] at hY' ⊢

Premises used: HomotopicalAlgebra.bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence p
⊢ weakEquivalences C p

Tactic:
rwa [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
⊢ IsIso (L.map p)

Tactic:
have := Localization.inverts L (weakEquivalences _) p
      (by rwa [← weakEquivalence_iff])
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
inr :
  Function.Bijective (α := LeftHomotopyClass X Y') (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)

Tactic:
rw [← Function.Bijective.of_comp_iff _
      (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence _ p)]

Premises used: HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, Function.Bijective.of_comp_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_1 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
⊢ Function.Bijective (α := LeftHomotopyClass X Y') (β := L.obj X ⟶ L.obj Y)
    ((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
      leftHomotopyClassToHom L)

Tactic:
(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))).bijective.comp hY'

Premises used: Equiv.bijective, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, Function.Bijective.comp, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_2 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
h :
  Eq (α := LeftHomotopyClass X Y' → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)
    ((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
      leftHomotopyClassToHom L)
⊢ Function.Bijective (α := LeftHomotopyClass X Y') (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)

Tactic:
convert! (Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))).bijective.comp hY'

Premises used: Equiv.bijective, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, Function.Bijective.comp, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
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
this_1 :
  ∀ (Y : C) [IsFibrant.{v_1, u_1} Y] (h : IsCofibrant.{v_1, u_1} Y),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsCofibrant.{v_1, u_1} Y
Y' : C
w : IsCofibrant.{v_1, u_1} Y'
p : Y' ⟶ Y
left : Fibration p
right : WeakEquivalence p
h_2 : IsFibrant.{v_1, u_1} Y'
hY' : Function.Bijective (α := LeftHomotopyClass X Y') (leftHomotopyClassToHom L)
this : IsIso (L.map p)
h :
  ∀ (f : LeftHomotopyClass X Y'),
    Eq (α := L.obj X ⟶ L.obj Y)
      (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
        (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) f)
      (((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
          leftHomotopyClassToHom L)
        f)
⊢ Eq (α := LeftHomotopyClass X Y' → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L) fun (f : LeftHomotopyClass X Y') ↦
      f.postcomp p)
    ((⇑(Iso.homCongr (Iso.refl (L.obj X)) (asIso (L.map p))) : (a : L.obj X ⟶ L.obj Y') → L.obj X ⟶ L.obj Y) ∘
      leftHomotopyClassToHom L)

Tactic:
ext f