no goals
m : Nat
⊢ lcm m m = m
match eq_zero_or_pos m with
| .inl h => rw [h, lcm_zero_left]
| .inr h => simp [lcm, Nat.mul_div_cancel _ h]
no goals
m : Nat
h : m = 0
⊢ lcm m m = m
rw [h, lcm_zero_left]
no goals
m : Nat
h : m > 0
⊢ lcm m m = m
simp [lcm, Nat.mul_div_cancel _ h]