awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : Fibration f₁
h₂ : Fibration f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
rw :
  ∀ (h₁ : fibrations C f₁) (h₂ : fibrations C f₂) [inst_7 : HasBinaryProduct.{v, u} X₁ X₂]
    [inst_8 : HasBinaryProduct.{v, u} Y₁ Y₂],
    fibrations C (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)
⊢ Fibration (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)

Tactic:
rw [fibration_iff] at h₁ h₂ ⊢

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
hf :
  functorCategory.{v, 0, 0, u} (fibrations C) (Discrete WalkingPair) (X := pair X₁ X₂) (Y := pair Y₁ Y₂) (mapPair f₁ f₂)
⊢ fibrations C (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)

Tactic:
apply MorphismProperty.limMap

Premises used: CategoryTheory.MorphismProperty.limMap
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
⊢ fibrations.{v, u} C (X := Functor.obj.{0, v, 0, u} (pair X₁ X₂) { as := WalkingPair.left : Discrete WalkingPair })
    (Y := Functor.obj.{0, v, 0, u} (pair Y₁ Y₂) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair f₁ f₂) { as := WalkingPair.left })

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
⊢ fibrations.{v, u} C (X := Functor.obj.{0, v, 0, u} (pair X₁ X₂) { as := WalkingPair.right : Discrete WalkingPair })
    (Y := Functor.obj.{0, v, 0, u} (pair Y₁ Y₂) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair f₁ f₂) { as := WalkingPair.right })

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsIso f
⊢ llp (fibrations C) f

Tactic:
have := (fibrations C).llp_of_isIso f
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsIso f
this : llp (fibrations C) f
⊢ trivialCofibrations C f

Tactic:
rw [fibrations_llp] at this

Premises used: HomotopicalAlgebra.fibrations_llp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsIso f
this : trivialCofibrations C f
⊢ Cofibration f

Tactic:
simpa only [cofibration_iff] using this.1

Premises used: And.left, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_5 : IsIso f
⊢ rlp (cofibrations C) f

Tactic:
have := (cofibrations C).rlp_of_isIso f
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_5 : IsIso f
this : rlp (cofibrations C) f
⊢ trivialFibrations C f

Tactic:
rw [cofibrations_rlp] at this

Premises used: HomotopicalAlgebra.cofibrations_rlp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_5 : IsIso f
this : trivialFibrations C f
⊢ Fibration f

Tactic:
simpa only [fibration_iff] using this.1

Premises used: HomotopicalAlgebra.fibration_iff, And.left
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
have : ∀ (h : MapFactorizationData (trivialCofibrations C) (fibrations C) f), WeakEquivalence f
⊢ WeakEquivalence f

Tactic:
have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) f
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
rw : weakEquivalences C f
⊢ WeakEquivalence f

Tactic:
rw [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ weakEquivalences C f

Tactic:
MorphismProperty.of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi.2

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.fac, And.right, CategoryTheory.MorphismProperty.of_retract, CategoryTheory.MorphismProperty.MapFactorizationData.hi, CategoryTheory.RetractArrow.ofLeftLiftingProperty
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ weakEquivalences C f

Tactic:
exact MorphismProperty.of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi.2

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.fac, And.right, CategoryTheory.MorphismProperty.of_retract, CategoryTheory.MorphismProperty.MapFactorizationData.hi, CategoryTheory.RetractArrow.ofLeftLiftingProperty
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x : C
rw : WeakEquivalence.{v, u} (𝟙 x)
⊢ weakEquivalences.{v, u} C (𝟙 x)

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x : C
⊢ WeakEquivalence.{v, u} (𝟙 x)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x x_1 : C
x_2 : x ⟶ x_1
h : IsIso x_2
rw : WeakEquivalence x_2
⊢ weakEquivalences C x_2

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x x_1 : C
x_2 : x ⟶ x_1
h : IsIso x_2
⊢ WeakEquivalence x_2

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : ContainsIdentities.{v, u} (weakEquivalences C)
X : C
rw : weakEquivalences.{v, u} C (𝟙 X)
⊢ WeakEquivalence.{v, u} (𝟙 X)

Tactic:
rw [weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : ContainsIdentities.{v, u} (weakEquivalences C)
X : C
⊢ weakEquivalences.{v, u} C (𝟙 X)

Tactic:
apply id_mem

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) f
⊢ Cofibration (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
simpa only [cofibration_iff] using h.hi

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.hi, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) f
⊢ Fibration (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
simpa only [fibration_iff] using h.hp.1

Premises used: HomotopicalAlgebra.fibration_iff, And.left, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (cofibrations C) (trivialFibrations C) f
⊢ WeakEquivalence (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
simpa only [weakEquivalence_iff] using h.hp.2

Premises used: HomotopicalAlgebra.weakEquivalence_iff, And.right, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
simpa only [cofibration_iff] using h.hi.1

Premises used: And.left, CategoryTheory.MorphismProperty.MapFactorizationData.hi, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ WeakEquivalence (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
simpa only [weakEquivalence_iff] using h.hi.2

Premises used: HomotopicalAlgebra.weakEquivalence_iff, And.right, CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
simpa only [fibration_iff] using h.hp

Premises used: HomotopicalAlgebra.fibration_iff, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X : C
⊢ IsCofibrant.{v_1, u_1} X ↔ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (cofibrations C)
A X : C
i : A ⟶ X
hA : IsInitial.{v_1, u_1} A
simp : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X) ↔ cofibrations C i
⊢ IsCofibrant.{v_1, u_1} X ↔ Cofibration i

Tactic:
simp only [cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (cofibrations C)
A X : C
i : A ⟶ X
hA : IsInitial.{v_1, u_1} A
apply : Arrow.mk (X := initial.{v_1, u_1} C) (initial.to X) ≅ Arrow.mk i
⊢ cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X) ↔ cofibrations C i

Tactic:
apply (cofibrations C).arrow_mk_iso_iff

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, HomotopicalAlgebra.cofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (cofibrations C)
A X : C
i : A ⟶ X
hA : IsInitial.{v_1, u_1} A
⊢ Arrow.mk (X := initial.{v_1, u_1} C) (initial.to X) ≅ Arrow.mk i

Tactic:
exact Arrow.isoMk (IsInitial.uniqueUpToIso initialIsInitial hA) (Iso.refl _)

Premises used: CategoryTheory.Limits.IsInitial.uniqueUpToIso, CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (cofibrations C)
X Y : C
i : X ⟶ Y
inst_4 : Cofibration i
hX : IsCofibrant.{v_1, u_1} X
⊢ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)

Tactic:
rw [isCofibrant_iff] at hX ⊢

Premises used: HomotopicalAlgebra.isCofibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (cofibrations C)
X Y : C
i : X ⟶ Y
inst_4 : Cofibration i
hX : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
rw : Cofibration (X := initial.{v_1, u_1} C) (initial.to X ≫ i)
⊢ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)

Tactic:
rw [Subsingleton.elim (initial.to Y) (initial.to X ≫ i)]

Premises used: CategoryTheory.Limits.initial.to, CategoryTheory.CategoryStruct.comp, Subsingleton.elim
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (cofibrations C)
X Y : C
i : X ⟶ Y
inst_4 : Cofibration i
hX : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
⊢ Cofibration (X := initial.{v_1, u_1} C) (initial.to X ≫ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : IsCofibrant.{v_1, u_1} Y
⊢ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)

Tactic:
rw [isCofibrant_iff] at hY

Premises used: HomotopicalAlgebra.isCofibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)
rw :
  ∀ (hY : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to Y)),
    cofibrations.{v_1, u_1} C (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl
⊢ Cofibration.{v_1, u_1} (C := C) (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl

Tactic:
rw [cofibration_iff] at hY ⊢

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to Y)
⊢ cofibrations.{v_1, u_1} C (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl

Tactic:
MorphismProperty.of_isPushout
    ((IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial).flip) hY

Premises used: CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.initialIsInitial, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, CategoryTheory.IsPushout.flip, CategoryTheory.Limits.pair
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to Y)
⊢ cofibrations.{v_1, u_1} C (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl

Tactic:
exact MorphismProperty.of_isPushout
    ((IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial).flip) hY

Premises used: CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.initialIsInitial, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, CategoryTheory.IsPushout.flip, CategoryTheory.Limits.pair
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : IsCofibrant.{v_1, u_1} X
⊢ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)

Tactic:
rw [isCofibrant_iff] at hX

Premises used: HomotopicalAlgebra.isCofibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
rw :
  ∀ (hX : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X)),
    cofibrations.{v_1, u_1} C (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr
⊢ Cofibration.{v_1, u_1} (C := C) (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr

Tactic:
rw [cofibration_iff] at hX ⊢

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X)
⊢ cofibrations.{v_1, u_1} C (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr

Tactic:
MorphismProperty.of_isPushout
    (IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial) hX

Premises used: CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.initialIsInitial, CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial, CategoryTheory.Limits.pair