English
If gauge t x ≠ 0, then the gauge with respect to t of the rescaled point equals the gauge with respect to s of x: gauge t (gaugeRescale s t x) = gauge s x.
Русский
Если gauge t x ≠ 0, то gauge_t(gaugeRescale_s_t(x)) = gauge_s(x).
LaTeX
$$$\\operatorname{gauge}_t\\big(\\operatorname{gaugeRescale}(s,t,x)\\big) = \\operatorname{gauge}_s(x) \\quad\\text{assuming } \\operatorname{gauge}(t,x) \\neq 0$$$
Lean4
theorem gauge_gaugeRescale' (s : Set E) {t : Set E} {x : E} (hx : gauge t x ≠ 0) :
gauge t (gaugeRescale s t x) = gauge s x := by
rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)), smul_eq_mul,
div_mul_cancel₀ _ hx]