awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X : C
⊢ IsFibrant.{v_1, u_1} X ↔ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from 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 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
simp : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X) ↔ fibrations C p
⊢ IsFibrant.{v_1, u_1} X ↔ Fibration p

Tactic:
simp only [fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
symm : fibrations C p ↔ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)
⊢ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X) ↔ fibrations C p

Tactic:
symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
apply : Arrow.mk p ≅ Arrow.mk (Y := terminal.{v_1, u_1} C) (terminal.from X)
⊢ fibrations C p ↔ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)

Tactic:
apply (fibrations C).arrow_mk_iso_iff

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
⊢ Arrow.mk p ≅ Arrow.mk (Y := terminal.{v_1, u_1} C) (terminal.from X)

Tactic:
exact Arrow.isoMk (Iso.refl _) (IsTerminal.uniqueUpToIso hY terminalIsTerminal)

Premises used: CategoryTheory.Limits.IsTerminal.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 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
inst_4 : Fibration p
hY : IsFibrant.{v_1, u_1} Y
⊢ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)

Tactic:
rw [isFibrant_iff] at hY ⊢

Premises used: HomotopicalAlgebra.isFibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
inst_4 : Fibration p
hY : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
rw : Fibration (Y := terminal.{v_1, u_1} C) (p ≫ terminal.from Y)
⊢ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)

Tactic:
rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y)]

Premises used: CategoryTheory.Limits.terminal.from, CategoryTheory.CategoryStruct.comp, Subsingleton.elim
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
inst_4 : Fibration p
hY : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
⊢ Fibration (Y := terminal.{v_1, u_1} C) (p ≫ terminal.from Y)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : IsFibrant.{v_1, u_1} Y
⊢ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)

Tactic:
rw [isFibrant_iff] at hY

Premises used: HomotopicalAlgebra.isFibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
rw :
  ∀ (hY : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from Y)),
    fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.fst
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.fst

Tactic:
rw [fibration_iff] at hY ⊢

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from Y)
⊢ fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.fst

Tactic:
MorphismProperty.of_isPullback
    (IsPullback.of_isLimit_binaryFan_of_isTerminal
      (limit.isLimit (pair X Y)) terminalIsTerminal).flip hY

Premises used: CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.IsPullback.flip, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from Y)
⊢ fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.fst

Tactic:
exact MorphismProperty.of_isPullback
    (IsPullback.of_isLimit_binaryFan_of_isTerminal
      (limit.isLimit (pair X Y)) terminalIsTerminal).flip hY

Premises used: CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.IsPullback.flip, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : IsFibrant.{v_1, u_1} X
⊢ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)

Tactic:
rw [isFibrant_iff] at hX

Premises used: HomotopicalAlgebra.isFibrant_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)
rw :
  ∀ (hX : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)),
    fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.snd
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.snd

Tactic:
rw [fibration_iff] at hX ⊢

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)
⊢ fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.snd

Tactic:
MorphismProperty.of_isPullback
    (IsPullback.of_isLimit_binaryFan_of_isTerminal
      (limit.isLimit (pair X Y)) terminalIsTerminal) hX

Premises used: CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)
⊢ fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.snd

Tactic:
exact MorphismProperty.of_isPullback
    (IsPullback.of_isLimit_binaryFan_of_isTerminal
      (limit.isLimit (pair X Y)) terminalIsTerminal) hX

Premises used: CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal, CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
⊢ CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
have sq' : CommSq (𝟙 X) (pushout.inl _ _ ≫ h.i) p h.p := .mk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
have h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p) := by simpa
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ cofibrations C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
have h₂ := comp_mem _ _ _ ((cofibrations C).of_isPushout
      (IsPushout.of_hasPushout f i) (mem_cofibrations i)) h.hi
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : cofibrations C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [← cofibration_iff] at h₂

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
rw :
  ∀
    (h₁ :
      weakEquivalences C
        ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
          h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
    (h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))),
    weakEquivalences C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
rw [weakEquivalence_iff] at h₁ ⊢

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  weakEquivalences C
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ weakEquivalences C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
of_postcomp _ _ _ h.hp.2 h₁

Premises used: And.right, CategoryTheory.MorphismProperty.of_postcomp, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  weakEquivalences C
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ weakEquivalences C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
exact of_postcomp _ _ _ h.hp.2 h₁

Premises used: And.right, CategoryTheory.MorphismProperty.of_postcomp, CategoryTheory.MorphismProperty.MapFactorizationData.hp