awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
f : X ⟶ Y
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) =
    ((Equiv.trans BifibrantObject.HoCat.homEquivRight
            (Equiv.trans E.fullyFaithfulFunctor.homEquiv
              (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y)))) :
          Equiv.{v_1 + 1, v_2 + 1} (RightHomotopyClass X Y)
            (Functor.obj (C := BifibrantObject.{v_1, u_1} C) (BifibrantObject.ι ⋙ L) (BifibrantObject.mk X) ⟶
              Functor.obj (C := BifibrantObject.{v_1, u_1} C) (BifibrantObject.ι ⋙ L) (BifibrantObject.mk Y))) :
        (a : RightHomotopyClass X Y) →
          (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
      (RightHomotopyClass.mk f)

Tactic:
(NatIso.naturality_1 e (BifibrantObject.homMk f)).symm

Premises used: CategoryTheory.NatIso.naturality_1, HomotopicalAlgebra.rightHomotopyClassToHom, HomotopicalAlgebra.BifibrantObject.homMk, Eq.symm
-- 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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
f : X ⟶ Y
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) =
    ((Equiv.trans BifibrantObject.HoCat.homEquivRight
            (Equiv.trans E.fullyFaithfulFunctor.homEquiv
              (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y)))) :
          Equiv.{v_1 + 1, v_2 + 1} (RightHomotopyClass X Y)
            (Functor.obj (C := BifibrantObject.{v_1, u_1} C) (BifibrantObject.ι ⋙ L) (BifibrantObject.mk X) ⟶
              Functor.obj (C := BifibrantObject.{v_1, u_1} C) (BifibrantObject.ι ⋙ L) (BifibrantObject.mk Y))) :
        (a : RightHomotopyClass X Y) →
          (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
      (RightHomotopyClass.mk f)

Tactic:
exact (NatIso.naturality_1 e (BifibrantObject.homMk f)).symm

Premises used: CategoryTheory.NatIso.naturality_1, HomotopicalAlgebra.BifibrantObject.homMk, Eq.symm
-- 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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
⊢ Eq (α := RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (rightHomotopyClassToHom L)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))

Tactic:
have : rightHomotopyClassToHom L =
      (BifibrantObject.HoCat.homEquivRight.trans (E.fullyFaithfulFunctor.homEquiv.trans
        (Iso.homCongr (e.app (.mk X)) (e.app (.mk Y))))) := by
    ext f
    obtain ⟨f, rfl⟩ := RightHomotopyClass.mk_surjective f
    exact (NatIso.naturality_1 e (BifibrantObject.homMk f)).symm
-- 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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
this :
  Eq (α := RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (rightHomotopyClassToHom L)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
rw :
  Function.Bijective.{v_1 + 1, v_2 + 1} (α := RightHomotopyClass X Y) (β := L.obj X ⟶ L.obj Y)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
rw [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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
this :
  Eq (α := RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (rightHomotopyClassToHom L)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
⊢ Function.Bijective.{v_1 + 1, v_2 + 1} (α := RightHomotopyClass X Y) (β := L.obj X ⟶ L.obj Y)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))

Tactic:
Equiv.bijective _

Premises used: Equiv.bijective
-- 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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_1 : IsFibrant.{v_1, u_1} X
E : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} (BifibrantObject.HoCat.{v_1, u_1} C) H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject.{v_1, u_1} C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L)
    (weakEquivalences (BifibrantObject.{v_1, u_1} C))
this :
  Eq (α := RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)) (rightHomotopyClassToHom L)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))
⊢ Function.Bijective.{v_1 + 1, v_2 + 1} (α := RightHomotopyClass X Y) (β := L.obj X ⟶ L.obj Y)
    (⇑(Equiv.trans BifibrantObject.HoCat.homEquivRight
          (Equiv.trans E.fullyFaithfulFunctor.homEquiv
            (Iso.homCongr (e.app (BifibrantObject.mk X)) (e.app (BifibrantObject.mk Y))))) :
      (a : RightHomotopyClass X Y) →
        (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk X) ⟶ (BifibrantObject.ι ⋙ L).obj (BifibrantObject.mk Y))

Tactic:
exact Equiv.bijective _

Premises used: Equiv.bijective
-- 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
rw : Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)

Tactic:
rw [bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom]

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
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
bijective_rightHomotopyClassToHom L X Y

Premises used: HomotopicalAlgebra.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
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
exact bijective_rightHomotopyClassToHom L X Y

Premises used: HomotopicalAlgebra.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
f : L.obj X ⟶ L.obj Y
mk :
  ∀ (w : LeftHomotopyClass X Y) (f : X ⟶ Y),
    ∃ (a : X ⟶ Y), L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)
⊢ ∃ (a : X ⟶ Y), L.map a = f

Tactic:
obtain ⟨⟨f⟩, rfl⟩ := (bijective_leftHomotopyClassToHom L X Y).2 f

Premises used: And.right, HomotopicalAlgebra.bijective_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
inst_4 : IsCofibrant.{v_1, u_1} X
inst_5 : IsFibrant.{v_1, u_1} Y
w : LeftHomotopyClass X Y
f : X ⟶ Y
⊢ ∃ (a : X ⟶ Y), L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)

Tactic:
⟨f, rfl⟩

Premises used: Exists.intro, 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
w : LeftHomotopyClass X Y
f : X ⟶ Y
⊢ ∃ (a : X ⟶ Y), L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)

Tactic:
exact ⟨f, 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 g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩

Premises used: CategoryTheory.AreEqualizedByLocalization.map_eq, HomotopicalAlgebra.RightHomotopyRel.factorsThroughLocalization, Iff.intro
-- 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 g : X ⟶ Y
refine : ∀ (h : L.map f = L.map g), RightHomotopyRel f g
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
-- 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 g : X ⟶ Y
h : L.map f = L.map g
rw : Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk f) (RightHomotopyClass.mk g)
⊢ RightHomotopyRel f g

Tactic:
rw [← RightHomotopyClass.mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_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
f g : X ⟶ Y
h : L.map f = L.map g
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) = rightHomotopyClassToHom L (RightHomotopyClass.mk g)

Tactic:
simpa
-- 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 g : X ⟶ Y
h : L.map f = L.map g
⊢ Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk f) (RightHomotopyClass.mk g)

Tactic:
exact (bijective_rightHomotopyClassToHom L X Y).1 (by simpa)

Premises used: And.left, HomotopicalAlgebra.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
f g : X ⟶ Y
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g

Tactic:
⟨fun h ↦ (LeftHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩

Premises used: CategoryTheory.AreEqualizedByLocalization.map_eq, HomotopicalAlgebra.LeftHomotopyRel.factorsThroughLocalization, Iff.intro
-- 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 g : X ⟶ Y
refine : ∀ (h : L.map f = L.map g), LeftHomotopyRel f g
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (LeftHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
-- 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 g : X ⟶ Y
h : L.map f = L.map g
rw : Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk f) (LeftHomotopyClass.mk g)
⊢ LeftHomotopyRel f g

Tactic:
rw [← LeftHomotopyClass.mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_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
f g : X ⟶ Y
h : L.map f = L.map g
⊢ leftHomotopyClassToHom L (LeftHomotopyClass.mk f) = leftHomotopyClassToHom L (LeftHomotopyClass.mk g)

Tactic:
simpa
-- 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 g : X ⟶ Y
h : L.map f = L.map g
⊢ Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk f) (LeftHomotopyClass.mk g)

Tactic:
exact (bijective_leftHomotopyClassToHom L X Y).1 (by simpa)

Premises used: And.left, HomotopicalAlgebra.bijective_leftHomotopyClassToHom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (sq.lift ≫ Q.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (P.π ≫ f) h.h) prod.fst

Tactic:
have := sq.fac_right =≫ prod.fst
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (sq.lift ≫ Q.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (P.π ≫ f) h.h) prod.fst
⊢ sq.lift ≫ Q.p₀ = P.π ≫ f

Tactic:
rw [Category.assoc, Q.p_fst, prod.lift_fst] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_fst, HomotopicalAlgebra.PrepathObject.p_fst, HomotopicalAlgebra.PathObject.toPrepathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p₀ = P.π ≫ f
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : LeftHomotopyRel f g
Q : PathObject.{v, u} Y
inst_3 : Q.IsGood
P : Cylinder.{v, u} X := ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g))
h : ⋯.choose (p := fun (P : Cylinder.{v, u} X) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)).LeftHomotopy f g
h' : ⋯.choose (p := fun (P' : Cylinder.{v, u} X) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)).IsGood
sq : CommSq (Z := Limits.prod.{v, u} Y Y) (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (sq.lift ≫ Q.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (P.π ≫ f) h.h) prod.snd

Tactic:
have := sq.fac_right =≫ prod.snd