no goals
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
⊢ lcm m n ∣ k
match eq_zero_or_pos k with
| .inl h => rw [h]; exact Nat.dvd_zero _
| .inr kpos =>
  apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
  rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
  exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ lcm m n ∣ 0
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ lcm m n ∣ k
rw [h]
no goals
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
h : k = 0
⊢ lcm m n ∣ 0
exact Nat.dvd_zero _
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ gcd m n * lcm m n ∣ gcd m n * k
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ lcm m n ∣ k
apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m * n ∣ gcd (m * k) (k * n)
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ gcd m n * lcm m n ∣ gcd m n * k
rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
no goals
m n k : Nat
H1 : m ∣ k
H2 : n ∣ k
kpos : k > 0
⊢ m * n ∣ gcd (m * k) (k * n)
exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)