F : Type u_2
ι : Type ?u.82971
α : Type ?u.82974
β : Type ?u.82977
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m
r : ℚ
⊢ ↑f ↑↑r.den = ↑g ↑↑r.den
F : Type u_2
ι : Type ?u.82971
α : Type ?u.82974
β : Type ?u.82977
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m
r : ℚ
⊢ ↑f r = ↑g r
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_ofNat,
  eq_on_inv₀ f g]
no goals
F : Type u_2
ι : Type ?u.82971
α : Type ?u.82974
β : Type ?u.82977
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m
r : ℚ
⊢ ↑f ↑↑r.den = ↑g ↑↑r.den
apply h