awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
inst_6 : HasBinaryCoproducts.{v, u} C
inst_7 : P.IsVeryGood
dsimp : Fibration P.π
⊢ Fibration P.symm.π

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
inst_6 : HasBinaryCoproducts.{v, u} C
inst_7 : P.IsVeryGood
⊢ Fibration P.π

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : Cylinder.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} A A)
    (codiag A)
⊢ Cofibration (X := coprod.{v, u} A A) (ofFactorizationData h).i

Tactic:
simpa using inferInstanceAs (Cofibration h.i)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : Cylinder.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} A A)
    (codiag A)
dsimp : Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ Fibration (ofFactorizationData h).π

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : Cylinder.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} A A)
    (codiag A)
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : Cylinder.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} A A)
    (codiag A)
inst_2 : HasTerminal.{v, u} C
inst_3 : IsFibrant.{v, u} A
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
⊢ IsFibrant.{v, u} (ofFactorizationData h).I

Tactic:
isFibrant_of_fibration (ofFactorizationData h).π

Premises used: HomotopicalAlgebra.Precylinder.π, HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.isFibrant_of_fibration, HomotopicalAlgebra.Cylinder.ofFactorizationData
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
⊢ ∃ (P : Cylinder.{v, u} A), P.IsVeryGood

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

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

Tactic:
⟨(exists_very_good A).choose⟩

Premises used: HomotopicalAlgebra.Cylinder.exists_very_good, Nonempty.intro, Exists.choose
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
⊢ P.i₁ ≫ P.π = P'.i₀ ≫ P'.π

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
simp : WeakEquivalence.{v, u} (𝟙 A)
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))

Tactic:
simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]

Premises used: CategoryTheory.Category.assoc, HomotopicalAlgebra.Precylinder.i₀_π, CategoryTheory.Limits.PushoutCocone.mk_ι_app, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence.{v, u} (𝟙 A)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))

Tactic:
have : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫
        pushout.desc P.π P'.π (by simp)) := by
      simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]
      infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))
dsimp : WeakEquivalence (X := pushout P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯)
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))
⊢ WeakEquivalence (X := pushout P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯)

Tactic:
apply weakEquivalence_of_precomp (P.i₀ ≫ pushout.inl _ _)

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.weakEquivalence_of_precomp, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pushout.inl, HomotopicalAlgebra.Precylinder.i₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (P.trans P').i (coprod.map P.i₀ (𝟙 A) ≫ ψ)

Tactic:
simp [Precylinder.i, ψ]

Premises used: HomotopicalAlgebra.Precylinder.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
rw : Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)
⊢ Cofibration (X := coprod.{v, u} A A) (P.trans P').i

Tactic:
rw [show (P.trans P').i = coprod.map P.i₀ (𝟙 A) ≫ ψ by simp [Precylinder.i, ψ]]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
    CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (P'.i ≫ pushout.inr P.i₁ P'.i₀)
h₂ :
  CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
    CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (P'.i ≫ pushout.inr P.i₁ P'.i₀)
⊢ Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
    CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (P'.i ≫ pushout.inr P.i₁ P'.i₀)

Tactic:
simp [ψ, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
    CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (P'.i ≫ pushout.inr P.i₁ P'.i₀)

Tactic:
simp [ψ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)

Tactic:
have fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr _ _ := by
      ext
      · simp [ψ, pushout.condition]
      · simp [ψ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
⊢ IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)

Tactic:
simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀

Premises used: CategoryTheory.IsPushout.of_hasPushout, HomotopicalAlgebra.Precylinder.i₁, HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.Precylinder.i₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
⊢ IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)

Tactic:
have sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr _ _) := by
      simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
rw : cofibrations C ψ
⊢ Cofibration ψ

Tactic:
rw [cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
rw : Cofibration (X := coprod.{v, u} A A) P'.i
⊢ cofibrations C (X := coprod.{v, u} A A) P'.i

Tactic:
rw [← cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (X := coprod.{v, u} A A) P'.i

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ cofibrations C ψ

Tactic:
exact (cofibrations C).of_isPushout
        (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
        (by rw [← cofibration_iff]; infer_instance)

Premises used: CategoryTheory.IsPushout.of_top, HomotopicalAlgebra.Precylinder.i₁, CategoryTheory.MorphismProperty.of_isPushout, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.of_coprod_inl_with_id
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration ψ

Tactic:
have : Cofibration ψ := by
      rw [cofibration_iff]
      exact (cofibrations C).of_isPushout
        (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
        (by rw [← cofibration_iff]; infer_instance)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
this : Cofibration ψ
⊢ Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R :
  LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
⊢ WeakEquivalence (R.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))

Tactic:
simpa only [weakEquivalence_iff] using R.hw

Premises used: HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.LocalizerMorphism.LeftResolution.hw
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
⊢ weakEquivalences.{u_2, u_1} C (X :=
    Functor.obj.{u_2, u_2, u_1, u_1} (C := CofibrantObject.{u_2, u_1} C)
      (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (mk (HoCat.resolutionObj.{u_2, u_1} X)))
    (HoCat.pResolutionObj X)

Tactic:
simpa using mem_weakEquivalences (HoCat.pResolutionObj X)

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, HomotopicalAlgebra.mem_weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
R :
  LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
⊢ Eq (α := initial.{u_2, u_1} C ⟶ X)
    (initial.to
        (Functor.obj
          (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
            (localizerMorphism C))
          (R₀.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))) ≫
      R₀.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
    (initial.to
        (Functor.obj
          (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
            (localizerMorphism C))
          (R.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))) ≫
      R.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
R :
  LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
⊢ CommSq (W := initial.{u_2, u_1} C)
    (initial.to
      (Functor.obj
        (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
          (localizerMorphism C))
        (R₀.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
    (initial.to
      (Functor.obj
        (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
          (localizerMorphism C))
        (R.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
    (R₀.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
    (R.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))

Tactic:
have sq : CommSq (initial.to _) (initial.to _) R₀.w R.w := ⟨by simp⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
R :
  LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
sq :
  CommSq (W := initial.{u_2, u_1} C)
    (initial.to
      (Functor.obj
        (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
          (localizerMorphism C))
        (R₀.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
    (initial.to
      (Functor.obj
        (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
          (localizerMorphism C))
        (R.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
    (R₀.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
    (R.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
⊢ Nonempty (Zigzag R R₀)

Tactic:
⟨Zigzag.of_hom { f := homMk (sq.lift) }⟩

Premises used: CategoryTheory.CommSq.lift, Nonempty.intro, HomotopicalAlgebra.CofibrantObject.homMk, CategoryTheory.LocalizerMorphism.LeftResolution.Hom.mk, CategoryTheory.Zigzag.of_hom