awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
have : WeakEquivalence (pushout.inl f i ≫ h.i) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_postcomp _ _ _ h.hp.2 h₁
-- 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))
this : WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ i ≫ pushout.inr f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ sq'.lift = f

Tactic:
simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.CommSq.fac_left, CategoryTheory.Limits.pushout.condition_assoc
-- 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))
this : WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := pushout.inr f i ≫ h.i ≫ sq'.lift
              fac_left := by
                simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left }⟩⟩
-- 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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
⊢ CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)

Tactic:
have sq' : CommSq h.i i (h.p ≫ pullback.snd _ _) (𝟙 B) := .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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
⊢ WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
⊢ WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
have h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g) := 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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
have h₂ := comp_mem _ _ _ h.hp ((fibrations C).of_isPullback
      (IsPullback.of_hasPullback p g) (mem_fibrations p))
-- 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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
rw [← fibration_iff] at h₂

Premises used: HomotopicalAlgebra.fibration_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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
rw :
  ∀
    (h₁ :
      weakEquivalences C
        (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
          h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g))
    (h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)),
    weakEquivalences C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  weakEquivalences C
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ weakEquivalences C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
of_precomp _ _ _ h.hi.2 h₁

Premises used: CategoryTheory.MorphismProperty.of_precomp, And.right, CategoryTheory.MorphismProperty.MapFactorizationData.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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  weakEquivalences C
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ weakEquivalences C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
exact of_precomp _ _ _ h.hi.2 h₁

Premises used: CategoryTheory.MorphismProperty.of_precomp, And.right, CategoryTheory.MorphismProperty.MapFactorizationData.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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)

Tactic:
have : WeakEquivalence (h.p ≫ pullback.snd p g) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_precomp _ _ _ h.hi.2 h₁
-- 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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
rw : sq'.lift ≫ (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
rw₁ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g ≫ p = g
rw₂ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g ≫ g = g
rw₃ rw₄ : g = g
⊢ (sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g

Tactic:
rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.fac_right, CategoryTheory.Limits.pullback.condition
-- 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} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [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 i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := sq'.lift ≫ h.p ≫ pullback.fst p g
              fac_right := by
                rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right] }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X : C
P : Precylinder.{v, u} X
Y : C
f₀ f₁ f₂ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
P' : Precylinder.{v, u} X
h' : P'.LeftHomotopy f₁ f₂
inst_1 : HasPushout P.i₁ P'.i₀
⊢ P.i₁ ≫ h.h = P'.i₀ ≫ h'.h

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
dsimp : Q.i₀.hom ≫ h.h.hom = f.hom
⊢ (Q.map P.ι).i₀ ≫ h.h.hom = f.hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
⊢ Q.i₀.hom ≫ h.h.hom = f.hom

Tactic:
simp only [← h.h₀, ObjectProperty.FullSubcategory.comp_hom]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom