x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ d * Nat.lcm x y = d * m
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ (fun x x_1 => x * x_1) d (Nat.lcm x y) = (fun x x_1 => x * x_1) d m
dsimp only
no goals
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ d * Nat.lcm x y = d * m
rw [← dm, ← hd, Nat.gcd_mul_lcm]