no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ lcm ↑(Units.mkOfMulEqOne a c (_ : a * c = 1)) ↑(Units.mkOfMulEqOne b d (_ : b * d = 1)) = 1
rw [lcm_units_coe_left, normalize_coe_units]