awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
have :
  ∀
    (this :
      Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ)
        (F ⋙ G)),
    LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
      weakEquivalences C) (localizerMorphism C)
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
have : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this_1 :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
this :
  Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
E : Hcof ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ)
      (𝟭 Hcof) (F ⋙ G)
      ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫ associator ι HoCat.resolution Lcofπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
⊢ F.IsEquivalence

Tactic:
have : F.IsEquivalence := E.isEquivalence_functor
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this_1 :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
this_2 :
  Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
E : Hcof ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ)
      (𝟭 Hcof) (F ⋙ G)
      ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫ associator ι HoCat.resolution Lcofπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
this : F.IsEquivalence
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lcof L F

Premises used: HomotopicalAlgebra.CofibrantObject.localizerMorphism, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
Hcof : Type u_1 :=
  MorphismProperty.Localization.{v_1, u_1} (C := HoCat.{v_1, u_1} C) (weakEquivalences (HoCat.{v_1, u_1} C))
Lcofπ : HoCat.{v_1, u_1} C ⥤ Hcof := MorphismProperty.Q (weakEquivalences (HoCat.{v_1, u_1} C))
Lcof : CofibrantObject.{v_1, u_1} C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := MorphismProperty.Localization.{v_1, u_1} (weakEquivalences C)
L : C ⥤ H := MorphismProperty.Q (weakEquivalences C)
F : Hcof ⥤ H :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))
    Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator toHoCat Lcofπ F)
G : H ⥤ Hcof :=
  LocalizerMorphism.localizedFunctor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
    (HoCat.localizerMorphismResolution C) L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := weakEquivalences C) (W₂ := weakEquivalences (HoCat.{v_1, u_1} C))
      (HoCat.localizerMorphismResolution C))
    L Lcofπ G
this_1 :
  Localization.Lifting L (weakEquivalences C) (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L))
    (G ⋙ F)
this_2 :
  Localization.Lifting Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G)
E : Hcof ≌ H :=
  CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences (CofibrantObject.{v_1, u_1} C)) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ)
      (𝟭 Hcof) (F ⋙ G)
      ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫ associator ι HoCat.resolution Lcofπ))
    (Localization.liftNatIso L (weakEquivalences C)
      (comp (D := HoCat.{v_1, u_1} C) HoCat.resolution (HoCat.toLocalization L)) L (G ⋙ F) (𝟭 H)
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
this : F.IsEquivalence
⊢ LocalizerMorphism.IsLocalizedEquivalence (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
exact LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lcof L F

Premises used: HomotopicalAlgebra.CofibrantObject.localizerMorphism, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : CofibrantObject.{v_1, u_1} C
dsimp : IsCofibrant.{v_1, u_1} (X.obj (P := cofibrantObjects C))
⊢ IsCofibrant.{v_1, u_1}
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      X)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : CofibrantObject.{v_1, u_1} C
⊢ IsCofibrant.{v_1, u_1} (X.obj (P := cofibrantObjects C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
L : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization (weakEquivalences C)
⊢ Functor.IsLocalization (C := CofibrantObject.{v_1, u_1} C) (ι ⋙ L) (weakEquivalences (CofibrantObject.{v_1, u_1} C))

Tactic:
inferInstanceAs (((localizerMorphism C).functor ⋙ L).IsLocalization _)

Premises used: _private.0.HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences._proof_1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P P' : Precylinder.{v, u} A
inst_1 : HasPushout P.i₁ P'.i₀
⊢ P.i₁ ≫ P.π = P'.i₀ ≫ P'.π

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : Precylinder.{v, u} A
inst_1 : HasBinaryCoproduct.{v, u} A A
⊢ CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P.i = P.i₀

Tactic:
simp [i]

Premises used: HomotopicalAlgebra.Precylinder.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P : Precylinder.{v, u} A
inst_1 : HasBinaryCoproduct.{v, u} A A
⊢ CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr P.i = P.i₁

Tactic:
simp [i]

Premises used: HomotopicalAlgebra.Precylinder.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P_1 : Precylinder.{v, u} A
X : C
P : Precylinder.{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.i₀ ≫ F.map P.π = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder
Goal:
C : Type u
inst : Category.{v, u} C
A : C
P_1 : Precylinder.{v, u} A
X : C
P : Precylinder.{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.i₁ ≫ F.map P.π = 𝟙 (F.obj X)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
dsimp : WeakEquivalence P.π
⊢ WeakEquivalence 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
⊢ WeakEquivalence P.π

Tactic:
infer_instance
-- 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 : HasBinaryCoproducts.{v, u} C
⊢ Eq (α := coprod.{v, u} A A ⟶ P.symm.I) (P.symm.i : coprod.{v, u} A A ⟶ P.symm.I)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I)

Tactic:
P.toPrecylinder.symm_i

Premises used: HomotopicalAlgebra.Precylinder.symm, HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.Precylinder.symm_i
-- 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 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
⊢ WeakEquivalence P.i₀

Tactic:
weakEquivalence_of_postcomp_of_fac P.i₀_π

Premises used: HomotopicalAlgebra.Precylinder.i₀_π, HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac
-- 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 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
⊢ WeakEquivalence P.i₁

Tactic:
weakEquivalence_of_postcomp_of_fac P.i₁_π

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac, HomotopicalAlgebra.Precylinder.i₁_π
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
rw : Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P.i)
⊢ Cofibration P.i₀

Tactic:
rw [← P.inl_i]

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.Precylinder.inl_i
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
⊢ Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P.i)

Tactic:
infer_instance
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
rw : Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr P.i)
⊢ Cofibration P.i₁

Tactic:
rw [← P.inr_i]

Premises used: HomotopicalAlgebra.Precylinder.inr_i, HomotopicalAlgebra.Cylinder.toPrecylinder
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
⊢ Cofibration (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr P.i)

Tactic:
infer_instance
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : HasInitial.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_6 : MorphismProperty.IsStableUnderCobaseChange.{v, u} (cofibrations C)
inst_7 : IsCofibrant.{v, u} A
inst_8 : P.IsGood
⊢ IsCofibrant.{v, u} P.I

Tactic:
isCofibrant_of_cofibration P.i₀

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.isCofibrant_of_cofibration, HomotopicalAlgebra.Precylinder.i₀
-- 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 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
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
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
⊢ 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
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} A
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
⊢ cofibrations C (X := coprod.{v, u} A A) P.i

Tactic:
have hi : cofibrations C P.i := by rw [← cofibration_iff]; infer_instance
-- 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 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
rw :
  cofibrations C (X := coprod.{v, u} A A)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I)
⊢ Cofibration (X := coprod.{v, u} A A) P.symm.i

Tactic:
rw [P.symm_i, cofibration_iff]

Premises used: HomotopicalAlgebra.Cylinder.symm_i, HomotopicalAlgebra.cofibration_iff
-- 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 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
⊢ cofibrations C (X := coprod.{v, u} A A)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I)

Tactic:
((cofibrations C).arrow_mk_iso_iff ?_).2 hi

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, HomotopicalAlgebra.cofibrations
-- 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 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
refine :
  Arrow.mk (X := coprod.{v, u} A A)
      (CategoryStruct.comp (Y := coprod.{v, u} A A)
          (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
        coprod.{v, u} A A ⟶ P.I) ≅
    Arrow.mk (X := coprod.{v, u} A A) P.i
⊢ cofibrations C (X := coprod.{v, u} A A)
    (CategoryStruct.comp (Y := coprod.{v, u} A A)
        (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
      coprod.{v, u} A A ⟶ P.I)

Tactic:
refine ((cofibrations C).arrow_mk_iso_iff ?_).2 hi

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, HomotopicalAlgebra.cofibrations
-- 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 : HasBinaryCoproducts.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (cofibrations C)
hi : cofibrations C (X := coprod.{v, u} A A) P.i
⊢ Arrow.mk (X := coprod.{v, u} A A)
      (CategoryStruct.comp (Y := coprod.{v, u} A A)
          (Iso.hom (coprod.braiding A A) : coprod.{v, u} A A ⟶ coprod.{v, u} A A) (P.i : coprod.{v, u} A A ⟶ P.I) :
        coprod.{v, u} A A ⟶ P.I) ≅
    Arrow.mk (X := coprod.{v, u} A A) P.i

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- 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 : HasBinaryCoproduct.{v, u} A A
inst_6 : HasTerminal.{v, u} C
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsVeryGood
⊢ IsFibrant.{v, u} P.I

Tactic:
isFibrant_of_fibration P.π

Premises used: HomotopicalAlgebra.Precylinder.π, HomotopicalAlgebra.Cylinder.toPrecylinder, HomotopicalAlgebra.isFibrant_of_fibration