awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 : 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)
have 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))
Tactic: obtain ⟨f, rfl⟩ := f.mk_surjective
Cleared hypotheses: 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_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))
have 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
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_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 : 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
have 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)
Tactic: obtain ⟨f, rfl⟩ := RightHomotopyClass.mk_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (hypothesis)
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))
⊢ Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have 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))
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
-- 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_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 (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
have 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))
Tactic: rw [this]
-- 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
⊢ Function.Bijective (α := LeftHomotopyClass X Y) (leftHomotopyClassToHom L)
have rw : Function.Bijective (α := RightHomotopyClass X Y) (rightHomotopyClassToHom L)
Tactic: rw [bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom]
-- 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 : L.obj X ⟶ L.obj Y
⊢ ∃ (a : X ⟶ Y), L.map a = f
have mk : ∀ (w : LeftHomotopyClass X Y) (f : X ⟶ Y), ∃ (a : X ⟶ Y), L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)
Tactic: obtain ⟨⟨f⟩, rfl⟩ := (bijective_leftHomotopyClassToHom L X Y).2 f
Cleared hypotheses: 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 g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g
have refine : ∀ (h : L.map f = L.map g), RightHomotopyRel f g
Tactic: refine ⟨fun h ↦ (RightHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
-- 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 g : X ⟶ Y
h : L.map f = L.map g
⊢ RightHomotopyRel f g
have rw : Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk f) (RightHomotopyClass.mk g)
Tactic: rw [← RightHomotopyClass.mk_eq_mk_iff]
-- 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 g : X ⟶ Y
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g
have refine : ∀ (h : L.map f = L.map g), LeftHomotopyRel f g
Tactic: refine ⟨fun h ↦ (LeftHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
-- 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 g : X ⟶ Y
h : L.map f = L.map g
⊢ LeftHomotopyRel f g
have rw : Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk f) (LeftHomotopyClass.mk g)
Tactic: rw [← LeftHomotopyClass.mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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)
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f
have 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
Tactic: have := sq.fac_right =≫ prod.fst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f
have this₁ : sq.lift ≫ Q.p₀ = P.π ≫ f
Tactic: rw [Category.assoc, Q.p_fst, prod.lift_fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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)
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₁ = g
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift (P.π ≫ f) h.h) prod.snd
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₁ = g
have this₁ : sq.lift ≫ Q.p₁ = h.h
Tactic: rw [Category.assoc, Q.p_snd, prod.lift_snd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f g
⊢ RightHomotopyRel f g
have obtain : ∀ (P : PathObject.{v, u} Y), P.IsVeryGood → RightHomotopyRel f g
Tactic: obtain ⟨P, _⟩ := PathObject.exists_very_good Y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f
have this : CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (Q.i ≫ sq.lift) =
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (f ≫ P.ι) h.h)
Tactic: have := coprod.inl ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (f ≫ P.ι) h.h)
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f
have this₁ : Q.i₀ ≫ sq.lift = f ≫ P.ι
Tactic: rw [Q.inl_i_assoc, coprod.inl_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g
have this : CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (Q.i ≫ sq.lift) =
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (f ≫ P.ι) h.h)
Tactic: have := coprod.inr ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (hypothesis)
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 : IsFibrant.{v, u} Y
h_1 : RightHomotopyRel f g
Q : Cylinder.{v, u} X
inst_3 : Q.IsGood
P : PathObject.{v, u} Y :=
  ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g))
h : ⋯.choose (p := fun (P : PathObject.{v, u} Y) ↦ P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)).RightHomotopy f g
h' : ⋯.choose (p := fun (P' : PathObject.{v, u} Y) ↦ P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)).IsGood
sq : CommSq (W := coprod.{v, u} X X) (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this :
  CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (f ≫ P.ι) h.h)
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g
have this₁ : Q.i₁ ≫ sq.lift = h.h
Tactic: rw [Q.inr_i_assoc, coprod.inr_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : RightHomotopyRel f g
⊢ LeftHomotopyRel f g
have obtain : ∀ (P : Cylinder.{v, u} X), P.IsVeryGood → LeftHomotopyRel f g
Tactic: obtain ⟨P, _⟩ := Cylinder.exists_very_good X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
⊢ Function.Bijective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
have left : Function.Injective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
left : Function.Injective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
⊢ Function.Bijective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
have right : Function.Surjective (β := LeftHomotopyClass X Z) fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
g : Y ⟶ Z
inst_3 : Fibration g
inst_4 : WeakEquivalence g
f₀ f₁ : LeftHomotopyClass X Y
h :
  Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₀)
    ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₁)
⊢ f₀ = f₁
have left : ∀ (f₀ : X ⟶ Y)
  (h :
    Eq.{v + 1} (α := LeftHomotopyClass X Z) ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) (mk f₀))
      ((fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) f₁)),
  mk f₀ = f₁
Tactic: obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
Cleared hypotheses: f₀, h