case H
m k n : Nat
H1 : m ∣ k
H2 : coprime k n
⊢ gcd m n ∣ 1
m k n : Nat
H1 : m ∣ k
H2 : coprime k n
⊢ coprime m n
apply eq_one_of_dvd_one
case H
m k n : Nat
H1 : m ∣ k
H2 : gcd k n = 1
⊢ gcd m n ∣ 1
case H
m k n : Nat
H1 : m ∣ k
H2 : coprime k n
⊢ gcd m n ∣ 1
rw [coprime] at H2
case H
m k n : Nat
H1 : m ∣ k
H2 : gcd k n = 1
this : gcd m n ∣ gcd k n
⊢ gcd m n ∣ 1
case H
m k n : Nat
H1 : m ∣ k
H2 : gcd k n = 1
⊢ gcd m n ∣ 1
have := Nat.gcd_dvd_gcd_of_dvd_left n H1
no goals
case H
m k n : Nat
H1 : m ∣ k
H2 : gcd k n = 1
this : gcd m n ∣ gcd k n
⊢ gcd m n ∣ 1
rwa [← H2]