awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
rw :
  MorphismProperty.HasTwoOutOfThreeProperty (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))
⊢ MorphismProperty.HasTwoOutOfThreeProperty (C := Over.{v, u} S) (weakEquivalences (Over.{v, u} S))

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]

Premises used: CategoryTheory.MorphismProperty.over_eq_inverseImage, HomotopicalAlgebra.weakEquivalences_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
⊢ MorphismProperty.HasTwoOutOfThreeProperty (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (trivialCofibrations C) (fibrations C)
rw :
  MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (trivialCofibrations C))
    (MorphismProperty.over (fibrations C))
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (trivialCofibrations (Over.{v, u} S))
    (fibrations (Over.{v, u} S))

Tactic:
rw [fibrations_over_def, trivialCofibrations_over_eq]

Premises used: HomotopicalAlgebra.trivialCofibrations_over_eq, HomotopicalAlgebra.fibrations_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (trivialCofibrations C) (fibrations C)
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (trivialCofibrations C))
    (MorphismProperty.over (fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (cofibrations C) (trivialFibrations C)
rw :
  MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (cofibrations C))
    (MorphismProperty.over (trivialFibrations C))
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (cofibrations (Over.{v, u} S))
    (trivialFibrations (Over.{v, u} S))

Tactic:
rw [cofibrations_over_def, trivialFibrations_over_eq]

Premises used: HomotopicalAlgebra.trivialFibrations_over_eq, HomotopicalAlgebra.cofibrations_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (cofibrations C) (trivialFibrations C)
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (cofibrations C))
    (MorphismProperty.over (trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P P' : PrepathObject.{v, u} A
inst_1 : HasPullback P.p₁ P'.p₀
⊢ P.ι ≫ P.p₁ = P'.ι ≫ P'.p₀

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : PrepathObject.{v, u} A
inst_1 : HasBinaryProduct.{v, u} A A
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.fst = P.p₀

Tactic:
simp [p]

Premises used: HomotopicalAlgebra.PrepathObject.p
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : PrepathObject.{v, u} A
inst_1 : HasBinaryProduct.{v, u} A A
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.snd = P.p₁

Tactic:
simp [p]

Premises used: HomotopicalAlgebra.PrepathObject.p
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P_1 : PrepathObject.{v, u} A
X : C
P : PrepathObject.{v, u} X
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} C D
⊢ F.map P.ι ≫ F.map P.p₀ = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P_1 : PrepathObject.{v, u} A
X : C
P : PrepathObject.{v, u} X
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} C D
⊢ F.map P.ι ≫ F.map P.p₁ = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
dsimp : WeakEquivalence P.ι
⊢ WeakEquivalence P.symm.ι

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
⊢ WeakEquivalence P.ι

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
⊢ Eq (α := P.symm.P ⟶ Limits.prod.{v, u} A A) P.symm.p
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))

Tactic:
P.toPrepathObject.symm_p

Premises used: HomotopicalAlgebra.PrepathObject.symm_p, HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
⊢ WeakEquivalence P.p₀

Tactic:
weakEquivalence_of_precomp_of_fac P.ι_p₀

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.ι_p₀, HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
⊢ WeakEquivalence P.p₁

Tactic:
weakEquivalence_of_precomp_of_fac P.ι_p₁

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.ι_p₁, HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
rw : Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.fst)
⊢ Fibration P.p₀

Tactic:
rw [← P.p_fst]

Premises used: HomotopicalAlgebra.PrepathObject.p_fst, HomotopicalAlgebra.PathObject.toPrepathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
⊢ Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.fst)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
rw : Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.snd)
⊢ Fibration P.p₁

Tactic:
rw [← P.p_snd]

Premises used: HomotopicalAlgebra.PrepathObject.p_snd, HomotopicalAlgebra.PathObject.toPrepathObject
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
⊢ Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.snd)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
⊢ IsFibrant.{v, u} P.P

Tactic:
isFibrant_of_fibration P.p₀

Premises used: HomotopicalAlgebra.PrepathObject.p₀, HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.isFibrant_of_fibration
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
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
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
⊢ 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
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
⊢ fibrations C (Y := Limits.prod.{v, u} A A) P.p

Tactic:
have hp : fibrations C P.p := by rw [← fibration_iff]; infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
rw :
  fibrations C (Y := Limits.prod.{v, u} A A)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))
⊢ Fibration (Y := Limits.prod.{v, u} A A) P.symm.p

Tactic:
rw [P.symm_p, fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.PathObject.symm_p
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
⊢ fibrations C (Y := Limits.prod.{v, u} A A)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))

Tactic:
((fibrations C).arrow_mk_iso_iff ?_).2 hp

Premises used: Iff.mpr, HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
refine :
  Arrow.mk (Y := Limits.prod.{v, u} A A)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A))) ≅
    Arrow.mk (Y := Limits.prod.{v, u} A A) P.p
⊢ fibrations C (Y := Limits.prod.{v, u} A A)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))

Tactic:
refine ((fibrations C).arrow_mk_iso_iff ?_).2 hp

Premises used: Iff.mpr, HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
⊢ Arrow.mk (Y := Limits.prod.{v, u} A A)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A))) ≅
    Arrow.mk (Y := Limits.prod.{v, u} A A) P.p

Tactic:
exact Arrow.isoMk (Iso.refl _) (prod.braiding A A)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : CategoryWithFibrations.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_5 : HasBinaryProduct.{v, u} A A
inst_6 : HasInitial.{v, u} C
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsVeryGood
⊢ IsCofibrant.{v, u} P.P

Tactic:
isCofibrant_of_cofibration P.ι

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.isCofibrant_of_cofibration, HomotopicalAlgebra.PrepathObject.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : CategoryWithFibrations.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
inst_6 : HasBinaryProducts.{v, u} C
inst_7 : P.IsVeryGood
dsimp : Cofibration P.ι
⊢ Cofibration P.symm.ι

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : CategoryWithFibrations.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
inst_6 : HasBinaryProducts.{v, u} C
inst_7 : P.IsVeryGood
⊢ Cofibration 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 : PathObject.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} A A)
    (diag A)
⊢ Fibration (Y := Limits.prod.{v, u} A A) (ofFactorizationData h).p

Tactic:
simpa using inferInstanceAs (Fibration h.p)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : PathObject.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} A A)
    (diag A)
dsimp : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ Cofibration (ofFactorizationData h).ι

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : PathObject.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} A A)
    (diag A)
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

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 : PathObject.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} A A)
    (diag A)
inst_2 : HasInitial.{v, u} C
inst_3 : IsCofibrant.{v, u} A
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
⊢ IsCofibrant.{v, u} (ofFactorizationData h).P

Tactic:
isCofibrant_of_cofibration (ofFactorizationData h).ι

Premises used: HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.isCofibrant_of_cofibration, HomotopicalAlgebra.PathObject.ofFactorizationData, HomotopicalAlgebra.PrepathObject.ι
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
⊢ ∃ (P : PathObject.{v, u} A), P.IsVeryGood

Tactic:
⟨ofFactorizationData (MorphismProperty.factorizationData _ _ _),
    inferInstance⟩

Premises used: CategoryTheory.MorphismProperty.factorizationData, inferInstance, Exists.intro, HomotopicalAlgebra.PathObject.ofFactorizationData
-- Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : PathObject.{v, u} A
⊢ Nonempty (PathObject.{v, u} A)

Tactic:
⟨(exists_very_good A).choose⟩

Premises used: HomotopicalAlgebra.PathObject.exists_very_good, Nonempty.intro, Exists.choose
-- 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
⊢ P.ι ≫ P.p₁ = P'.ι ≫ P'.p₀

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
rw : WeakEquivalence.{v, u} (𝟙 A)
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))

Tactic:
rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]

Premises used: CategoryTheory.Limits.pullback.lift_fst_assoc, HomotopicalAlgebra.PrepathObject.ι_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
⊢ WeakEquivalence.{v, u} (𝟙 A)

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
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))

Tactic:
have : WeakEquivalence (pullback.lift P.ι P'.ι (by simp) ≫
        pullback.fst P.p₁ P'.p₀ ≫ P.p₀) := by
      rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]
      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
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))
dsimp : WeakEquivalence (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯)
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι

Tactic:
dsimp
-- 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
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))
⊢ WeakEquivalence (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯)

Tactic:
apply weakEquivalence_of_postcomp _ (pullback.fst P.p₁ P'.p₀ ≫ P.p₀)

Premises used: HomotopicalAlgebra.PrepathObject.p₀, HomotopicalAlgebra.weakEquivalence_of_postcomp, HomotopicalAlgebra.PathObject.toPrepathObject, HomotopicalAlgebra.PrepathObject.p₁, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp
-- 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) (P.trans P').p (ψ ≫ prod.map P.p₀ (𝟙 A))

Tactic:
simp [PrepathObject.p, ψ]

Premises used: HomotopicalAlgebra.PrepathObject.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₁)
rw : Fibration (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))
⊢ Fibration (Y := Limits.prod.{v, u} A A) (P.trans P').p

Tactic:
rw [show (P.trans P').p = ψ ≫ prod.map P.p₀ (𝟙 A) by simp [PrepathObject.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₁)
h₁ :
  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
h₂ :
  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
⊢ 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:
ext