Quantitative profile estimates do not depend on the particular regularity witness.

theorem EulerPacketCylinderField.ProfileBudget.of_profile_eq {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support support' : Set EulerSmoothLimit.Space} {a b : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (hG : ProfileBudget G S R p) (hTpos : 0 < T) (H : ProfileRegularity P T hT support' b) (he : a = b) : ProfileBudget H S R p