a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ False
a b : ℕ
hab : coprime a b
⊢ List.Disjoint (factors a) (factors b)
intro q hqa hqb
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime 1
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ False
apply not_prime_one
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime q
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime 1
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_factors hqa) (dvd_of_mem_factors hqb)]
no goals
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime q
exact prime_of_mem_factors hqa