a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
a b k : ℕ
h_ab_coprime : coprime a b
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
rw [coprime_iff_gcd_eq_one] at h_ab_coprime
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ gcd a b
⊢ k = 1
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
have h1 := dvd_gcd hka hkb
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ 1
⊢ k = 1
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ gcd a b
⊢ k = 1
rw [h_ab_coprime] at h1
no goals
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ 1
⊢ k = 1
exact Nat.dvd_one.mp h1