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 Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration g
inst_7 : WeakEquivalence g
⊢ weakEquivalences C (Y := pushout f g) (pushout.inl f g)

Tactic:
(MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g)
    (mem_trivialCofibrations g)).2

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, HomotopicalAlgebra.mem_trivialCofibrations, And.right
-- 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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration g
inst_7 : WeakEquivalence g
⊢ weakEquivalences C (Y := pushout f g) (pushout.inl f g)

Tactic:
exact (MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g)
    (mem_trivialCofibrations g)).2

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, HomotopicalAlgebra.mem_trivialCofibrations, And.right
-- 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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration f
inst_7 : WeakEquivalence f
rw : weakEquivalences C (Y := pushout f g) (pushout.inr f g)
⊢ WeakEquivalence (Y := pushout f g) (pushout.inr f g)

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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration f
inst_7 : WeakEquivalence f
⊢ weakEquivalences C (Y := pushout f g) (pushout.inr f g)

Tactic:
(MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g).flip
    (mem_trivialCofibrations f)).2

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, HomotopicalAlgebra.mem_trivialCofibrations, CategoryTheory.IsPushout.flip, And.right
-- 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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration f
inst_7 : WeakEquivalence f
⊢ weakEquivalences C (Y := pushout f g) (pushout.inr f g)

Tactic:
exact (MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g).flip
    (mem_trivialCofibrations f)).2

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout, HomotopicalAlgebra.mem_trivialCofibrations, CategoryTheory.IsPushout.flip, And.right
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hf : Fibration f
rw : ∀ (hf : fibrations C f), fibrations C (X := pullback f g) (pullback.snd f g)
⊢ Fibration (X := pullback f g) (pullback.snd f g)

Tactic:
rw [fibration_iff] at hf ⊢

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 Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hf : fibrations C f
⊢ fibrations C (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g) hf

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hf : fibrations C f
⊢ fibrations C (X := pullback f g) (pullback.snd f g)

Tactic:
exact MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g) hf

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hg : Fibration g
rw : ∀ (hg : fibrations C g), fibrations C (X := pullback f g) (pullback.fst f g)
⊢ Fibration (X := pullback f g) (pullback.fst f g)

Tactic:
rw [fibration_iff] at hg ⊢

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 Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hg : fibrations C g
⊢ fibrations C (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g).flip hg

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hg : fibrations C g
⊢ fibrations C (X := pullback f g) (pullback.fst f g)

Tactic:
exact MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g).flip hg

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration f
inst_7 : WeakEquivalence f
rw : weakEquivalences C (X := pullback f g) (pullback.snd f g)
⊢ WeakEquivalence (X := pullback f g) (pullback.snd f g)

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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration f
inst_7 : WeakEquivalence f
⊢ weakEquivalences C (X := pullback f g) (pullback.snd f g)

Tactic:
(MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g)
    (mem_trivialFibrations f)).2

Premises used: CategoryTheory.MorphismProperty.of_isPullback, And.right, CategoryTheory.IsPullback.of_hasPullback, HomotopicalAlgebra.mem_trivialFibrations
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration f
inst_7 : WeakEquivalence f
⊢ weakEquivalences C (X := pullback f g) (pullback.snd f g)

Tactic:
exact (MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g)
    (mem_trivialFibrations f)).2

Premises used: CategoryTheory.MorphismProperty.of_isPullback, And.right, CategoryTheory.IsPullback.of_hasPullback, HomotopicalAlgebra.mem_trivialFibrations
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration g
inst_7 : WeakEquivalence g
rw : weakEquivalences C (X := pullback f g) (pullback.fst f g)
⊢ WeakEquivalence (X := pullback f g) (pullback.fst f g)

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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration g
inst_7 : WeakEquivalence g
⊢ weakEquivalences C (X := pullback f g) (pullback.fst f g)

Tactic:
(MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g).flip
    (mem_trivialFibrations g)).2

Premises used: CategoryTheory.MorphismProperty.of_isPullback, And.right, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, HomotopicalAlgebra.mem_trivialFibrations
-- 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 Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration g
inst_7 : WeakEquivalence g
⊢ weakEquivalences C (X := pullback f g) (pullback.fst f g)

Tactic:
exact (MorphismProperty.of_isPullback (IsPullback.of_hasPullback f g).flip
    (mem_trivialFibrations g)).2

Premises used: CategoryTheory.MorphismProperty.of_isPullback, And.right, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback, HomotopicalAlgebra.mem_trivialFibrations
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
simp :
  ∀ (h : ∀ (i : J), cofibrations C (f i)),
    cofibrations C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
⊢ Cofibration (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)

Tactic:
simp only [cofibration_iff] at h ⊢

Premises used: 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
h : ∀ (i : J), cofibrations C (f i)
⊢ cofibrations C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)

Tactic:
MorphismProperty.colimMap _ (fun ⟨i⟩ ↦ h i)

Premises used: _private.0.HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations.match_1, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.as, HomotopicalAlgebra.cofibrations, CategoryTheory.Limits.Sigma.map, CategoryTheory.MorphismProperty.colimMap, CategoryTheory.NatTrans.app
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
h : ∀ (i : J), cofibrations C (f i)
⊢ cofibrations C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)

Tactic:
exact MorphismProperty.colimMap _ (fun ⟨i⟩ ↦ h i)

Premises used: CategoryTheory.MorphismProperty.colimMap
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
rw : weakEquivalences C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
⊢ WeakEquivalence (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)

Tactic:
(MorphismProperty.colimMap (W := (trivialCofibrations C)) _
    (fun ⟨i⟩ ↦ mem_trivialCofibrations (f i))).2

Premises used: And.right, CategoryTheory.Limits.Sigma.map, CategoryTheory.MorphismProperty.colimMap
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)

Tactic:
exact (MorphismProperty.colimMap (W := (trivialCofibrations C)) _
    (fun ⟨i⟩ ↦ mem_trivialCofibrations (f i))).2

Premises used: And.right, CategoryTheory.MorphismProperty.colimMap
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
simp :
  ∀ (h : ∀ (i : J), fibrations C (f i)),
    fibrations C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
⊢ Fibration (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)

Tactic:
simp only [fibration_iff] at 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h : ∀ (i : J), fibrations C (f i)
⊢ fibrations C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)

Tactic:
MorphismProperty.limMap _ (fun ⟨i⟩ ↦ h i)

Premises used: HomotopicalAlgebra.fibrations, _private.0.HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations.match_1, CategoryTheory.MorphismProperty.limMap, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.as, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Pi.map
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h : ∀ (i : J), fibrations C (f i)
⊢ fibrations C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)

Tactic:
exact MorphismProperty.limMap _ (fun ⟨i⟩ ↦ h i)

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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
rw : weakEquivalences C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
⊢ WeakEquivalence (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)

Tactic:
(MorphismProperty.limMap (W := (trivialFibrations C)) _
    (fun ⟨i⟩ ↦ mem_trivialFibrations (f i))).2

Premises used: CategoryTheory.MorphismProperty.limMap, And.right, CategoryTheory.Limits.Pi.map
-- 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
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)

Tactic:
exact (MorphismProperty.limMap (W := (trivialFibrations C)) _
    (fun ⟨i⟩ ↦ mem_trivialFibrations (f i))).2

Premises used: CategoryTheory.MorphismProperty.limMap, And.right
-- 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} (cofibrations C) (trivialFibrations C)
h₁ : Cofibration f₁
h₂ : Cofibration f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
rw :
  ∀ (h₁ : cofibrations C f₁) (h₂ : cofibrations C f₂) [inst_7 : HasBinaryCoproduct.{v, u} X₁ X₂]
    [inst_8 : HasBinaryCoproduct.{v, u} Y₁ Y₂],
    cofibrations C (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)
⊢ Cofibration (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)

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

Premises used: 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₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
hf :
  functorCategory.{v, 0, 0, u} (cofibrations C) (Discrete WalkingPair) (X := pair X₁ X₂) (Y := pair Y₁ Y₂)
    (mapPair f₁ f₂)
⊢ cofibrations C (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)

Tactic:
apply MorphismProperty.colimMap

Premises used: CategoryTheory.MorphismProperty.colimMap
-- 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} (cofibrations C) (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
⊢ cofibrations.{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} (cofibrations C) (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
⊢ cofibrations.{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