∀ (α : Type u) {β : Type v} [inst : Group α] [inst_1 : MulAction α β] (b : β),
  MulAction.orbitProdStabilizerEquivGroup α b =
    ((MulAction.orbitEquivQuotientStabilizer α b).prodCongr (Equiv.refl ↥(MulAction.stabilizer α b))).trans
      Subgroup.groupEquivQuotientProdSubgroup.symm