m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ gcd m n = 1
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ coprime m n
rw [coprime_iff_gcd_eq_one]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
⊢ False
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ gcd m n = 1
by_contra g2
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ False
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
⊢ False
obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ m

case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ n
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ False
apply H p hp <;> apply dvd_trans hpdvd
no goals
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ m
exact gcd_dvd_left _ _
no goals
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ n
exact gcd_dvd_right _ _