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 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)
f : LeftHomotopyClass X Y'
h :
  ∀ (f : X ⟶ Y'),
    Eq (α := L.obj X ⟶ L.obj Y)
      (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
        (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) (LeftHomotopyClass.mk f))
      (Function.comp (α := LeftHomotopyClass X 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) (LeftHomotopyClass.mk f))
⊢ 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)

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
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)
f : X ⟶ Y'
⊢ Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
      (fun (f : LeftHomotopyClass X Y') ↦ f.postcomp p) (LeftHomotopyClass.mk f))
    (Function.comp (α := LeftHomotopyClass X 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) (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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
inr :
  ∀
    (this :
      ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
        Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)),
    ¬IsFibrant.{v_1, u_1} X → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
wlog :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X],
    IsFibrant.{v_1, u_1} X → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
wlog _ : IsFibrant X generalizing X

Premises used: HomotopicalAlgebra.IsFibrant
-- 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
⊢ ∃ (X' : C) (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i ∧ IsFibrant.{v_1, u_1} X'

Tactic:
⟨_, FibrantObject.HoCat.iResolutionObj X, inferInstance, inferInstance, inferInstance⟩

Premises used: inferInstance, HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, And.intro, Exists.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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
inr :
  ∀ (X' : C) (i : X ⟶ X'),
    Cofibration i →
      WeakEquivalence i →
        IsFibrant.{v_1, u_1} X' → Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
obtain ⟨X', i, _, _, _⟩ : ∃ (X' : C) (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i ∧
        IsFibrant X' :=
      ⟨_, FibrantObject.HoCat.iResolutionObj X, inferInstance, inferInstance, 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
⊢ IsCofibrant.{v_1, u_1} X'

Tactic:
have _ := isCofibrant_of_cofibration i
-- 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
⊢ Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)

Tactic:
have hX' := this X' 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence i
⊢ weakEquivalences C i

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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
⊢ IsIso (L.map i)

Tactic:
have := Localization.inverts L (weakEquivalences _) i
      (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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
inr :
  Function.Bijective (α := RightHomotopyClass X' Y) (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)

Tactic:
rw [← Function.Bijective.of_comp_iff _
      (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence Y i)]

Premises used: Function.Bijective.of_comp_iff, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
-- 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Function.Bijective (α := RightHomotopyClass X' Y) (β := L.obj X ⟶ L.obj Y)
    ((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
      rightHomotopyClassToHom L)

Tactic:
(Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'

Premises used: Equiv.bijective, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, Function.Bijective.comp, Equiv.symm, 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h_1 : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_2 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_3 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
h :
  Eq (α := RightHomotopyClass X' Y → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)
    ((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
      rightHomotopyClassToHom L)
⊢ Function.Bijective (α := RightHomotopyClass X' Y) (β := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)

Tactic:
convert! (Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'

Premises used: Equiv.bijective, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, Function.Bijective.comp, Equiv.symm, 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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h_1 : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_2 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_3 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
h :
  ∀ (f : RightHomotopyClass X' Y),
    Eq (α := L.obj X ⟶ L.obj Y)
      (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
        (fun (g : RightHomotopyClass X' Y) ↦ g.precomp i) f)
      (((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
          rightHomotopyClassToHom L)
        f)
⊢ Eq (α := RightHomotopyClass X' Y → (L.obj X ⟶ L.obj Y))
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L) fun (g : RightHomotopyClass X' Y) ↦
      g.precomp i)
    ((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
      rightHomotopyClassToHom L)

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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h_1 : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_2 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_3 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
f : RightHomotopyClass X' Y
h :
  ∀ (f : X' ⟶ Y),
    Eq (α := L.obj X ⟶ L.obj Y)
      (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
        (fun (g : RightHomotopyClass X' Y) ↦ g.precomp i) (RightHomotopyClass.mk f))
      (Function.comp (α := RightHomotopyClass X' Y)
        (⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y)
        (rightHomotopyClassToHom L) (RightHomotopyClass.mk f))
⊢ Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (fun (g : RightHomotopyClass X' Y) ↦ g.precomp i) f)
    (((⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y) ∘
        rightHomotopyClassToHom L)
      f)

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

Premises used: HomotopicalAlgebra.RightHomotopyClass.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_1 : C
inst_4 : IsCofibrant.{v_1, u_1} X
Y : C
inst_5 : IsFibrant.{v_1, u_1} Y
h : IsCofibrant.{v_1, u_1} Y
this_1 :
  ∀ (X : C) [IsCofibrant.{v_1, u_1} X] (h : IsFibrant.{v_1, u_1} X),
    Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
h_1 : ¬IsFibrant.{v_1, u_1} X
X' : C
i : X ⟶ X'
left : Cofibration i
left_1 : WeakEquivalence i
right : IsFibrant.{v_1, u_1} X'
h_2 : IsCofibrant.{v_1, u_1} X'
hX' : Function.Bijective (α := RightHomotopyClass X' Y) (rightHomotopyClassToHom L)
this : IsIso (L.map i)
f : X' ⟶ Y
⊢ Eq (α := L.obj X ⟶ L.obj Y)
    (Function.comp (β := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
      (fun (g : RightHomotopyClass X' Y) ↦ g.precomp i) (RightHomotopyClass.mk f))
    (Function.comp (α := RightHomotopyClass X' Y)
      (⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm : (a : L.obj X' ⟶ L.obj Y) → L.obj X ⟶ L.obj Y)
      (rightHomotopyClassToHom L) (RightHomotopyClass.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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h_1 : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_2 : 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))
h :
  ∀ (f : RightHomotopyClass X Y),
    rightHomotopyClassToHom L 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))
        f
⊢ 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:
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_1 Y_1 Y : C
inst_4 : IsFibrant.{v_1, u_1} Y
h_1 : IsCofibrant.{v_1, u_1} Y
X : C
inst_5 : IsCofibrant.{v_1, u_1} X
h_2 : 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 : RightHomotopyClass X Y
h :
  ∀ (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)
⊢ rightHomotopyClassToHom L 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))
      f

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

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl