[GOAL]
p q : Primes
h : ↑p = ↑q
⊢ ↑p = ↑q
[PROOFSTEP]
injection h
[GOAL]
n m : ℕ+
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
let h := mul_pos n.pos m.pos
[GOAL]
n m : ℕ+
h : 0 < ↑n * ↑m := mul_pos (pos n) (pos m)
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
rw [← gcd_mul_lcm (n : ℕ) (m : ℕ), mul_comm] at h 
[GOAL]
n m : ℕ+
h : 0 < Nat.lcm ↑n ↑m * Nat.gcd ↑n ↑m
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
exact pos_of_dvd_of_pos (Dvd.intro (Nat.gcd (n : ℕ) (m : ℕ)) rfl) h
[GOAL]
n : ℕ+
⊢ n < 2 → n = 1
[PROOFSTEP]
intro h
[GOAL]
n : ℕ+
h : n < 2
⊢ n = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
case a n : ℕ+ h : n < 2 ⊢ 1 ≤ n
[PROOFSTEP]
swap
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n
case a n : ℕ+ h : n < 2 ⊢ n ≤ 1
[PROOFSTEP]
apply PNat.one_le
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
[PROOFSTEP]
exact PNat.lt_add_one_iff.1 h
[GOAL]
p m : ℕ+
pp : Prime p
⊢ m ∣ p ↔ m = 1 ∨ m = p
[PROOFSTEP]
rw [PNat.dvd_iff]
[GOAL]
p m : ℕ+
pp : Prime p
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
[PROOFSTEP]
rw [Nat.dvd_prime pp]
[GOAL]
p m : ℕ+
pp : Prime p
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
⊢ Prime p → p ≠ 1
[PROOFSTEP]
intro pp
[GOAL]
p : ℕ+
pp : Prime p
⊢ p ≠ 1
[PROOFSTEP]
intro contra
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ False
[PROOFSTEP]
apply Nat.Prime.ne_one pp
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ ↑p = 1
[PROOFSTEP]
rw [PNat.coe_eq_one_iff]
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ p = 1
[PROOFSTEP]
apply contra
[GOAL]
p : ℕ+
pp : Prime p
⊢ ¬p ∣ 1
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
p : ℕ+
pp : Prime p
⊢ ¬↑p ∣ ↑1
[PROOFSTEP]
apply Nat.Prime.not_dvd_one pp
[GOAL]
n : ℕ+
hn : n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ { val := p, property := (_ : 0 < p) } ∣ n
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ ↑{ val := p, property := (_ : 0 < p) } ∣ ↑n
[PROOFSTEP]
apply hp
[GOAL]
m n : ℕ+
⊢ coprime ↑m ↑n ↔ Coprime m n
[PROOFSTEP]
unfold coprime Coprime
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ gcd m n = 1
[PROOFSTEP]
rw [← coe_inj]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ ↑(gcd m n) = ↑1
[PROOFSTEP]
simp
[GOAL]
k m n : ℕ+
⊢ Coprime m k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ Coprime m k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
[PROOFSTEP]
rw [mul_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime (↑m * ↑n) ↑k
[PROOFSTEP]
apply Nat.coprime.mul
[GOAL]
k m n : ℕ+
⊢ Coprime k m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ Coprime k m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime ↑k ↑(m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime ↑k ↑(m * n)
[PROOFSTEP]
rw [mul_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime (↑k) (↑m * ↑n)
[PROOFSTEP]
apply Nat.coprime.mul_right
[GOAL]
m n : ℕ+
⊢ gcd m n = gcd n m
[PROOFSTEP]
apply eq
[GOAL]
case a
m n : ℕ+
⊢ ↑(gcd m n) = ↑(gcd n m)
[PROOFSTEP]
simp only [gcd_coe]
[GOAL]
case a
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = Nat.gcd ↑n ↑m
[PROOFSTEP]
apply Nat.gcd_comm
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd m n = m
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m n : ℕ+
⊢ ↑m ∣ ↑n ↔ gcd m n = m
[PROOFSTEP]
rw [Nat.gcd_eq_left_iff_dvd]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = ↑m ↔ gcd m n = m
[PROOFSTEP]
rw [← coe_inj]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = ↑m ↔ ↑(gcd m n) = ↑m
[PROOFSTEP]
simp
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd n m = m
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd m n = m
[PROOFSTEP]
apply gcd_eq_left_iff_dvd
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
[PROOFSTEP]
intro h
[GOAL]
m n k : ℕ+
h : Coprime k n
⊢ gcd (k * m) n = gcd m n
[PROOFSTEP]
apply eq
[GOAL]
case a
m n k : ℕ+
h : Coprime k n
⊢ ↑(gcd (k * m) n) = ↑(gcd m n)
[PROOFSTEP]
simp only [gcd_coe, mul_coe]
[GOAL]
case a
m n k : ℕ+
h : Coprime k n
⊢ Nat.gcd (↑k * ↑m) ↑n = Nat.gcd ↑m ↑n
[PROOFSTEP]
apply Nat.coprime.gcd_mul_left_cancel
[GOAL]
case a.H
m n k : ℕ+
h : Coprime k n
⊢ coprime ↑k ↑n
[PROOFSTEP]
simpa
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (m * k) n = gcd m n
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (k * n) = gcd m n
[PROOFSTEP]
intro h
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
[PROOFSTEP]
iterate 2 rw [gcd_comm]; symm;
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd m n
[PROOFSTEP]
symm
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m n = gcd (k * n) m
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd n m = gcd (k * n) m
[PROOFSTEP]
symm
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd n m
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel _ h
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (n * k) = gcd m n
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (k * n) = gcd m n
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel_right
[GOAL]
n : ℕ+
⊢ gcd 1 n = 1
[PROOFSTEP]
rw [← gcd_eq_left_iff_dvd]
[GOAL]
n : ℕ+
⊢ 1 ∣ n
[PROOFSTEP]
apply one_dvd
[GOAL]
n : ℕ+
⊢ gcd n 1 = 1
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
n : ℕ+
⊢ gcd 1 n = 1
[PROOFSTEP]
apply one_gcd
[GOAL]
m n : ℕ+
⊢ Coprime m n → Coprime n m
[PROOFSTEP]
unfold Coprime
[GOAL]
m n : ℕ+
⊢ gcd m n = 1 → gcd n m = 1
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n : ℕ+
⊢ gcd n m = 1 → gcd n m = 1
[PROOFSTEP]
simp
[GOAL]
m k n : ℕ+
⊢ m ∣ k → Coprime k n → Coprime m n
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → Coprime m n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
[PROOFSTEP]
apply Nat.coprime.coprime_dvd_left
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
rw [gcd_eq_left_iff_dvd] at am 
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
conv_lhs => rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd a m = gcd (a * b) m
[PROOFSTEP]
rw [eq_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd (a * b) m = gcd a m
[PROOFSTEP]
apply Coprime.gcd_mul_right_cancel a
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ Coprime b m
[PROOFSTEP]
apply Coprime.coprime_dvd_left bn cop.symm
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (b * a) m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_left cop am bn
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd m (a * b)
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_left cop am bn
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd m (b * a)
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (b * a) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_right cop am bn
[GOAL]
k m n : ℕ+
h : Coprime m n
⊢ gcd k (m * n) = gcd k m * gcd k n
[PROOFSTEP]
rw [← coprime_coe] at h 
[GOAL]
k m n : ℕ+
h : coprime ↑m ↑n
⊢ gcd k (m * n) = gcd k m * gcd k n
[PROOFSTEP]
apply eq
[GOAL]
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ ↑(gcd k (m * n)) = ↑(gcd k m * gcd k n)
[PROOFSTEP]
simp only [gcd_coe, mul_coe]
[GOAL]
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ Nat.gcd (↑k) (↑m * ↑n) = Nat.gcd ↑k ↑m * Nat.gcd ↑k ↑n
[PROOFSTEP]
apply Nat.coprime.gcd_mul k h
[GOAL]
m n : ℕ+
⊢ m ∣ n → gcd m n = m
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m n : ℕ+
⊢ ↑m ∣ ↑n → gcd m n = m
[PROOFSTEP]
intro h
[GOAL]
m n : ℕ+
h : ↑m ∣ ↑n
⊢ gcd m n = m
[PROOFSTEP]
apply eq
[GOAL]
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ ↑(gcd m n) = ↑m
[PROOFSTEP]
simp only [gcd_coe]
[GOAL]
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ Nat.gcd ↑m ↑n = ↑m
[PROOFSTEP]
apply Nat.gcd_eq_left h
[GOAL]
m n : ℕ+
k l : ℕ
h : Coprime m n
⊢ coprime (↑m ^ k) (↑n ^ l)
[PROOFSTEP]
rw [← coprime_coe] at *
[GOAL]
m n : ℕ+
k l : ℕ
h : coprime ↑m ↑n
⊢ coprime (↑m ^ k) (↑n ^ l)
[PROOFSTEP]
apply Nat.coprime.pow
[GOAL]
case H1
m n : ℕ+
k l : ℕ
h : coprime ↑m ↑n
⊢ coprime ↑m ↑n
[PROOFSTEP]
apply h
