k n m : Nat
H1 : coprime k n
H2 : k ∣ m * n
t : k ∣ gcd (m * k) (m * n) := dvd_gcd (Nat.dvd_mul_left k m) H2
⊢ k ∣ m
k n m : Nat
H1 : coprime k n
H2 : k ∣ m * n
⊢ k ∣ m
let t := dvd_gcd (Nat.dvd_mul_left k m) H2
no goals
k n m : Nat
H1 : coprime k n
H2 : k ∣ m * n
t : k ∣ gcd (m * k) (m * n) := dvd_gcd (Nat.dvd_mul_left k m) H2
⊢ k ∣ m
rwa [gcd_mul_left, H1.gcd_eq_one, Nat.mul_one] at t