m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
⊢ False
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
⊢ lcm m n ≠ 0
intro h
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : gcd m n * lcm m n = m * n
⊢ False
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
⊢ False
have h1 := gcd_mul_lcm m n
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : 0 = m * n
⊢ False
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : gcd m n * lcm m n = m * n
⊢ False
rw [h, Nat.mul_zero] at h1
no goals
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : 0 = m * n
⊢ False
match mul_eq_zero.1 h1.symm with
| .inl hm1 => exact hm hm1
| .inr hn1 => exact hn hn1
no goals
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : 0 = m * n
hm1 : m = 0
⊢ False
exact hm hm1
no goals
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : lcm m n = 0
h1 : 0 = m * n
hn1 : n = 0
⊢ False
exact hn hn1