awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
⊢ IsStableUnderRetracts.{v, u} (rlp (cofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
⊢ IsStableUnderRetracts.{v, u} (trivialFibrations C)

Tactic:
have : (trivialFibrations C).IsStableUnderRetracts := by
    rw [← cofibrations_rlp]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
⊢ Arrow.Hom.left h.r ≫ f =
    hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
⊢ CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)

Tactic:
have sq : CommSq h.r.left hw.i f (hw.p ≫ h.r.right) := ⟨by simp⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
rwa rwa₁ rwa₂ rwa₃ : Fibration f
⊢ fibrations C f

Tactic:
rwa [← fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
⊢ fibrations C f

Tactic:
have hf : fibrations C f := by rwa [← fibration_iff]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
⊢ HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f

Tactic:
have : HasLiftingProperty hw.i f := hasLiftingProperty_of_wfs _ _ hw.hi hf
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this_1 : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
have : ∀ (this : RetractArrow f (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))), WeakEquivalence f
⊢ WeakEquivalence f

Tactic:
have : RetractArrow f hw.p :=
    { i := Arrow.homMk (h.i.left ≫ hw.i) h.i.right
      r := Arrow.homMk sq.lift h.r.right }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this_1 : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this_2 : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
this : RetractArrow f (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ trivialFibrations C (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have h' : trivialFibrations C hw.p :=
    ⟨hw.hp, (weakEquivalence_iff _).1 (weakEquivalence_of_precomp_of_fac hw.fac)⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_5 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst_7 : Fibration f
inst_8 : WeakEquivalence w
h : RetractArrow f w
hw : MapFactorizationData (trivialCofibrations C) (fibrations C) w
this_1 : IsStableUnderRetracts.{v, u} (trivialFibrations C)
sq :
  CommSq (Arrow.Hom.left h.r) (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
    (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this_2 : HasLiftingProperty (hw.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) f
this : RetractArrow f (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
h' : trivialFibrations C (hw.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence f

Tactic:
simpa only [weakEquivalence_iff] using (of_retract this h').2

Premises used: HomotopicalAlgebra.weakEquivalence_iff, And.right, CategoryTheory.MorphismProperty.of_retract
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : weakEquivalences C w
⊢ WeakEquivalence w

Tactic:
rw [← weakEquivalence_iff] at hw

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
have : ∀ (hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f), weakEquivalences C f
⊢ weakEquivalences C f

Tactic:
have hf := factorizationData (trivialCofibrations C) (fibrations C) f
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

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

Premises used: And.left, CategoryTheory.MorphismProperty.MapFactorizationData.hi, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have : Cofibration hf.i := by
      simpa only [cofibration_iff] using hf.hi.1
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

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

Premises used: HomotopicalAlgebra.weakEquivalence_iff, And.right, CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have : WeakEquivalence hf.i := by
      simpa only [weakEquivalence_iff] using hf.hi.2
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i =
    Arrow.Hom.left h.i ≫ w

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
⊢ Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
simpa only [fibration_iff] using hf.hp

Premises used: HomotopicalAlgebra.fibration_iff, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
⊢ Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
have : Fibration hf.p := by simpa only [fibration_iff] using hf.hp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)

Tactic:
simpa [φ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)

Tactic:
have : WeakEquivalence (pushout.inr _ _ ≫ φ) := by simpa [φ]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this : WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
⊢ WeakEquivalence φ

Tactic:
have := weakEquivalence_of_precomp (pushout.inr _ _) φ
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this : WeakEquivalence φ
⊢ hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      𝟙 (hf.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)) =
    Arrow.Hom.left h.i ≫ Arrow.Hom.left h.r ≫ hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)

Tactic:
simp