awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ IsIso (L.map P.ι)

Tactic:
have := Localization.inverts L (weakEquivalences C) P.ι (by
    rw [← weakEquivalence_iff]
    infer_instance)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
this : IsIso (L.map P.ι)
⊢ L.map P.p₀ = L.map P.p₁

Tactic:
simp [← cancel_epi (L.map P.ι), ← L.map_comp]

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, HomotopicalAlgebra.PrepathObject.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f : X ⟶ Y
⊢ RightHomotopyRel f f

Tactic:
⟨Classical.arbitrary _, ⟨PathObject.RightHomotopy.refl _ _⟩⟩

Premises used: Nonempty.intro, HomotopicalAlgebra.PathObject.RightHomotopy.refl, Exists.intro, Classical.arbitrary, HomotopicalAlgebra.RightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
Z : C
i : Z ⟶ X
obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g), RightHomotopyRel (i ≫ f) (i ≫ g)
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
Z : C
i : Z ⟶ X
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
(h.precomp i).rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel, HomotopicalAlgebra.PathObject.RightHomotopy.precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
Z : C
i : Z ⟶ X
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
exact (h.precomp i).rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel, HomotopicalAlgebra.PathObject.RightHomotopy.precomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
obtain :
  ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g),
    ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
⊢ ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
h.exists_good_pathObject

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
exact h.exists_good_pathObject

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : RightHomotopyRel f g
obtain :
  ∀ (P : PathObject.{v, u} Y),
    P.IsGood →
      ∀ (h : P.RightHomotopy f g), ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
rw : Fibration (Y := Limits.prod.{v, u} Y Y) (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p)
⊢ Fibration (Y := Limits.prod.{v, u} Y Y) P'.p

Tactic:
rw [show P'.p = fac.p ≫ P.p by cat_disch]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration (Y := Limits.prod.{v, u} Y Y) (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration (Y := Limits.prod.{v, u} Y Y) P'.p

Tactic:
have : Fibration P'.p := by
    rw [show P'.p = fac.p ≫ P.p by cat_disch]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
this : Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
⊢ CommSq (W := initial.{v, u} C) (initial.to (fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))) (initial.to X)
    (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) h.h

Tactic:
have sq : CommSq (initial.to _) (initial.to _) fac.p h.h := { }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
this : Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
sq :
  CommSq (W := initial.{v, u} C) (initial.to (fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))) (initial.to X)
    (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) h.h
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
⟨P', { }, ⟨{ h := sq.lift }⟩⟩

Premises used: CategoryTheory.CommSq.lift, HomotopicalAlgebra.PrepathObject.RightHomotopy.mk, Nonempty.intro, HomotopicalAlgebra.PathObject.IsVeryGood.mk, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
this : Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
sq :
  CommSq (W := initial.{v, u} C) (initial.to (fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))) (initial.to X)
    (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) h.h
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)

Tactic:
exact ⟨P', { }, ⟨{ h := sq.lift }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g), RightHomotopyRel g f
⊢ RightHomotopyRel g f

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel g f

Tactic:
h.symm.rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.symm, HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel g f

Tactic:
exact h.symm.rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.symm, HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : RightHomotopyRel f₀ f₁
h' : RightHomotopyRel f₁ f₂
obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f₀ f₁), RightHomotopyRel f₀ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h' : RightHomotopyRel f₁ f₂
P : PathObject.{v, u} Y
h : P.RightHomotopy f₀ f₁
obtain : ∀ (P' : PathObject.{v, u} Y), P'.IsGood → ∀ (h' : P'.RightHomotopy f₁ f₂), RightHomotopyRel f₀ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_pathObject

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h'_1 : RightHomotopyRel f₁ f₂
P : PathObject.{v, u} Y
h : P.RightHomotopy f₀ f₁
P' : PathObject.{v, u} Y
left : P'.IsGood
h' : P'.RightHomotopy f₁ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
(h.trans h').rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.trans, HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h'_1 : RightHomotopyRel f₁ f₂
P : PathObject.{v, u} Y
h : P.RightHomotopy f₀ f₁
P' : PathObject.{v, u} Y
left : P'.IsGood
h' : P'.RightHomotopy f₁ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
exact (h.trans h').rightHomotopyRel

Premises used: HomotopicalAlgebra.PathObject.RightHomotopy.trans, HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
obtain : ∀ (P : PathObject.{v, u} Y), P.IsVeryGood → ∀ (h : P.RightHomotopy f g), RightHomotopyRel (f ≫ p) (g ≫ p)
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject

Premises used: HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
obtain : ∀ (Q : PathObject.{v, u} Z), Q.IsVeryGood → RightHomotopyRel (f ≫ p) (g ≫ p)
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
obtain ⟨Q, _⟩ := PathObject.exists_very_good Z

Premises used: HomotopicalAlgebra.PathObject.exists_very_good
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
⊢ CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))

Tactic:
have sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) := { }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.fst

Tactic:
have := sq.fac_right =≫ prod.fst
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.fst
⊢ sq.lift ≫ Q.p₀ = P.p₀ ≫ p

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_fst, HomotopicalAlgebra.PrepathObject.p_fst, HomotopicalAlgebra.PathObject.toPrepathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : sq.lift ≫ Q.p₀ = P.p₀ ≫ p
⊢ (h.h ≫ sq.lift) ≫ Q.p₀ = f ≫ p

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.snd

Tactic:
have := sq.fac_right =≫ prod.snd
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.snd
⊢ sq.lift ≫ Q.p₁ = P.p₁ ≫ p

Tactic:
simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this

Premises used: HomotopicalAlgebra.PrepathObject.p_snd, CategoryTheory.Category.assoc, HomotopicalAlgebra.PathObject.toPrepathObject, CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : sq.lift ≫ Q.p₁ = P.p₁ ≫ p
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
exact ⟨Q,
   ⟨{ h := h.h ≫ sq.lift
      h₀ := by
        have := sq.fac_right =≫ prod.fst
        simp only [Category.assoc, prod.lift_fst, Q.p_fst] at this
        simp [this]
      h₁ := by
        have := sq.fac_right =≫ prod.snd
        simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
        simp [this]
    }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ Function.Surjective.{v + 1, v + 1} (α := X ⟶ Y) (β := RightHomotopyClass X Y) mk

Tactic:
Quot.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk, HomotopicalAlgebra.RightHomotopyClass, Quot.mk_surjective
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
⊢ Eq (α := RightHomotopyClass X Y) (mk f) (mk g)

Tactic:
Quot.sound h

Premises used: Quot.sound, HomotopicalAlgebra.RightHomotopyClass.mk, HomotopicalAlgebra.RightHomotopyClass
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := RightHomotopyClass X Z) (precomp (mk g) f) (mk (f ≫ g))

Tactic:
rfl

Premises used: HomotopicalAlgebra.RightHomotopyClass.precomp, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsFibrant.{v, u} Y
f g : X ⟶ Y
rw : Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen RightHomotopyRel f g
⊢ Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ RightHomotopyRel f g

Tactic:
rw [← (RightHomotopyRel.equivalence X Y).eqvGen_iff]

Premises used: HomotopicalAlgebra.RightHomotopyRel.equivalence, Equivalence.eqvGen_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsFibrant.{v, u} Y
f g : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen RightHomotopyRel f g

Tactic:
Quot.eq

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk, HomotopicalAlgebra.RightHomotopyClass, Quot.eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsFibrant.{v, u} Y
f g : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen RightHomotopyRel f g

Tactic:
exact Quot.eq

Premises used: Quot.eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z X Y : C
P : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.op.i₀ ≫ h.h.op).unop = f.op.unop

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z X Y : C
P : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.op.i₁ ≫ h.h.op).unop = g.op.unop

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : C
X Y : Cᵒᵖ
P : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.unop.i₀ ≫ h.h.unop).op = f.unop.op

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : C
X Y : Cᵒᵖ
P : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.unop.i₁ ≫ h.h.unop).op = g.unop.op

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z X Y : C
P : Precylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ Quiver.Hom.unop (h.h.op ≫ P.op.p₀) = f.op.unop

Tactic:
simp