awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (pullback.snd P.p₁ P'.p₀ ≫ P'.p) prod.fst

Tactic:
simp [ψ, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (pullback.snd P.p₁ P'.p₀ ≫ P'.p) prod.snd

Tactic:
simp [ψ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)

Tactic:
have fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd _ _ ≫ P'.p := by
      ext
      · simp [ψ, pullback.condition]
      · simp [ψ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
⊢ IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)

Tactic:
simpa [ψ] using IsPullback.of_hasPullback P.p₁ P'.p₀

Premises used: HomotopicalAlgebra.PrepathObject.p₀, HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.p₁, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
⊢ IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)

Tactic:
have sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst) := by
      simpa [ψ] using IsPullback.of_hasPullback P.p₁ P'.p₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
rw : fibrations C ψ
⊢ Fibration ψ

Tactic:
rw [fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
rw : Fibration (Y := Limits.prod.{v, u} A A) P'.p
⊢ fibrations C (Y := Limits.prod.{v, u} A A) P'.p

Tactic:
rw [← fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
⊢ Fibration (Y := Limits.prod.{v, u} A A) P'.p

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
⊢ fibrations C ψ

Tactic:
exact (fibrations C).of_isPullback
        (IsPullback.of_right sq fac (IsPullback.of_prod_fst_with_id P.p₁ A)).flip
          (by rw [← fibration_iff]; infer_instance)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.of_prod_fst_with_id, HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.p₁, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_right
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
⊢ Fibration ψ

Tactic:
have : Fibration ψ := by
      rw [fibration_iff]
      exact (fibrations C).of_isPullback
        (IsPullback.of_right sq fac (IsPullback.of_prod_fst_with_id P.p₁ A)).flip
          (by rw [← fibration_iff]; infer_instance)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
this : Fibration ψ
⊢ Fibration (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : PrepathObject.{v, u} A
⊢ Eq.{v + 1} (α := unop (op A) ⟶ unop (op A)) (Quiver.Hom.unop (P.p₀.op ≫ P.ι.op)) (Quiver.Hom.unop (𝟙 (op A)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : PrepathObject.{v, u} A
⊢ Eq.{v + 1} (α := unop (op A) ⟶ unop (op A)) (Quiver.Hom.unop (P.p₁.op ≫ P.ι.op)) (Quiver.Hom.unop (𝟙 (op A)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Cᵒᵖ
P : PrepathObject.{v, u} A
⊢ (P.p₀.unop ≫ P.ι.unop).op = Quiver.Hom.op (𝟙 (unop A))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Cᵒᵖ
P : PrepathObject.{v, u} A
⊢ (P.p₁.unop ≫ P.ι.unop).op = Quiver.Hom.op (𝟙 (unop A))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : Precylinder.{v, u} A
⊢ Eq.{v + 1} (α := unop (op A) ⟶ unop (op A)) (Quiver.Hom.unop (P.π.op ≫ P.i₀.op)) (Quiver.Hom.unop (𝟙 (op A)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : Precylinder.{v, u} A
⊢ Eq.{v + 1} (α := unop (op A) ⟶ unop (op A)) (Quiver.Hom.unop (P.π.op ≫ P.i₁.op)) (Quiver.Hom.unop (𝟙 (op A)))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Cᵒᵖ
P : Precylinder.{v, u} A
⊢ (P.π.unop ≫ P.i₀.unop).op = Quiver.Hom.op (𝟙 (unop A))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Cᵒᵖ
P : Precylinder.{v, u} A
⊢ (P.π.unop ≫ P.i₁.unop).op = Quiver.Hom.op (𝟙 (unop A))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y : C
P : PrepathObject.{v, u} Y
X : C
f₀ f₁ f₂ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
P' : PrepathObject.{v, u} Y
h' : P'.RightHomotopy f₁ f₂
inst_1 : HasPullback P.p₁ P'.p₀
⊢ h.h ≫ P.p₁ = h'.h ≫ P'.p₀

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
dsimp : h.h.hom ≫ Q.p₀.hom = f.hom
⊢ h.h.hom ≫ (Q.map P.ι).p₀ = f.hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ Q.p₀.hom = f.hom

Tactic:
simp only [← h.h₀, ObjectProperty.FullSubcategory.comp_hom]

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
dsimp : h.h.hom ≫ Q.p₁.hom = g.hom
⊢ h.h.hom ≫ (Q.map P.ι).p₁ = g.hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ Q.p₁.hom = g.hom

Tactic:
simp only [← h.h₁, ObjectProperty.FullSubcategory.comp_hom]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.comp_hom, HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
h₁ : (ObjectProperty.homMk (P := P) h.h ≫ Q.p₀).hom = f.hom
⊢ ObjectProperty.homMk (P := P) h.h ≫ Q.p₀ = f

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk (P := P) h.h ≫ Q.p₀).hom = f.hom

Tactic:
h.h₀

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk (P := P) h.h ≫ Q.p₀).hom = f.hom

Tactic:
exact h.h₀

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
h₁ : (ObjectProperty.homMk (P := P) h.h ≫ Q.p₁).hom = g.hom
⊢ ObjectProperty.homMk (P := P) h.h ≫ Q.p₁ = g

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk (P := P) h.h ≫ Q.p₁).hom = g.hom

Tactic:
h.h₁

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk (P := P) h.h ≫ Q.p₁).hom = g.hom

Tactic:
exact h.h₁

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} Y
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
mk : ∀ (h : X ⟶ P.P), h ≫ P.p₀ = f₀ → h ≫ P.p₁ = f₁ → (WeakEquivalence f₀ ↔ WeakEquivalence f₁)
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
induction h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} Y
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : X ⟶ P.P
h₀ : h ≫ P.p₀ = f₀
h₁ : h ≫ P.p₁ = f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
grind [weakEquivalence_postcomp_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_postcomp_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
rw :
  fibrations C (Y := Limits.prod.{v, u} Y Y)
    (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p
⊢ Fibration (Y := Limits.prod.{v, u} Y Y)
    (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p

Tactic:
rw [fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
⊢ fibrations C (d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
d.hp

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
h₁ :
  (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p =
    d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)
⊢ fibrations C (Y := Limits.prod.{v, u} Y Y)
    (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p

Tactic:
convert! d.hp

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
⊢ (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p =
    d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
⊢ ∃ (P' : PathObject.{v, u} Y), P'.IsGood ∧ Nonempty.{v + 1} (P'.RightHomotopy f g)

Tactic:
exact
   ⟨{ P := d.Z
      p₀ := d.p ≫ prod.fst
      p₁ := d.p ≫ prod.snd
      ι := P.ι ≫ d.i }, ⟨by
        rw [fibration_iff]
        convert! d.hp
        aesop⟩, ⟨{ h := h.h ≫ d.i }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A B X : C
P : PathObject.{v, u} B
f₀ f₁ : A ⟶ B
inst_2 : IsFibrant.{v, u} B
inst_3 : P.IsGood
h : P.RightHomotopy f₀ f₁
i : A ⟶ X
inst_4 : Cofibration i
l₀ : X ⟶ B
hl₀ : i ≫ l₀ = f₀
sq : CommSq h.h i P.p₀ l₀
⊢ i ≫ PrepathObject.RightHomotopy.h (f := l₀) { h := sq.lift, h₀ := ⋯, h₁ := ⋯ : P.RightHomotopy l₀ (sq.lift ≫ P.p₁) } =
    h.h

Tactic:
simp
-- 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
⊢ RightHomotopyRel f g

Tactic:
⟨_, ⟨h⟩⟩

Premises used: Nonempty.intro, Exists.intro, HomotopicalAlgebra.RightHomotopyRel
-- 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)
rw : L.map f = L.map g
⊢ AreEqualizedByLocalization (weakEquivalences C) f g

Tactic:
rw [areEqualizedByLocalization_iff L]

Premises used: CategoryTheory.areEqualizedByLocalization_iff
-- 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 : L.map P.p₀ = L.map P.p₁
⊢ L.map f = L.map g

Tactic:
simp only [← h.h₀, ← h.h₁, L.map_comp, this]

Premises used: HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀, CategoryTheory.Functor.map_comp, HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
-- 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)
suffices : L.map P.p₀ = L.map P.p₁
⊢ L.map f = L.map g

Tactic:
suffices L.map P.p₀ = L.map P.p₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]
-- 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)
rw : WeakEquivalence P.ι
⊢ weakEquivalences C P.ι

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- 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)
⊢ WeakEquivalence P.ι

Tactic:
infer_instance