rw [one_div_one_div, mul_comm, mul_comm_div, one_mul]
case h.e'_3.h.e'_7.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
x✝ : ℝ
⊢ g x✝ * f (x / x✝) / ↑x✝ = f (1 / x✝ * x) * g (1 / (1 / x✝)) / ↑x✝
no goals