m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
⊢ a / d = b / d ↔ a = b
refine ⟨fun h => ?_, congr_arg fun n => n / d⟩
no goals
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b
rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]