∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : HomotopicalAlgebra.ModelCategory C} {X Y : C}
  {f : X ⟶ Y}
  {toMapFactorizationData :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f}
  {r : toMapFactorizationData.Z ⟶ X}
  {i_r :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam}
  {fibration_r :
    autoParam (HomotopicalAlgebra.Fibration r) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam}
  {toMapFactorizationData_1 :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f}
  {r_1 : toMapFactorizationData_1.Z ⟶ X}
  {i_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData_1.i r_1 = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam}
  {fibration_r_1 :
    autoParam (HomotopicalAlgebra.Fibration r_1) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam},
  { toMapFactorizationData := toMapFactorizationData, r := r, i_r := i_r, fibration_r := fibration_r } =
      { toMapFactorizationData := toMapFactorizationData_1, r := r_1, i_r := i_r_1, fibration_r := fibration_r_1 } →
    toMapFactorizationData = toMapFactorizationData_1 ∧ r ≍ r_1