[GOAL]
m n k : ℕ
⊢ gcd m (n + k * m) = gcd m n
[PROOFSTEP]
simp [gcd_rec m (n + k * m), gcd_rec m n]
[GOAL]
m n k : ℕ
⊢ gcd m (n + m * k) = gcd m n
[PROOFSTEP]
simp [gcd_rec m (n + m * k), gcd_rec m n]
[GOAL]
m n k : ℕ
⊢ gcd m (k * m + n) = gcd m n
[PROOFSTEP]
simp [add_comm _ n]
[GOAL]
m n k : ℕ
⊢ gcd m (m * k + n) = gcd m n
[PROOFSTEP]
simp [add_comm _ n]
[GOAL]
m n k : ℕ
⊢ gcd (m + k * n) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (m + n * k) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_mul_left_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (k * n + m) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_mul_right_add_right, gcd_comm]
[GOAL]
m n k : ℕ
⊢ gcd (n * k + m) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_mul_left_add_right, gcd_comm]
[GOAL]
m n : ℕ
⊢ gcd m (n + m) = gcd m (n + 1 * m)
[PROOFSTEP]
rw [one_mul]
[GOAL]
m n : ℕ
⊢ gcd (m + n) n = gcd m n
[PROOFSTEP]
rw [gcd_comm, gcd_add_self_right, gcd_comm]
[GOAL]
m n : ℕ
⊢ gcd (m + n) m = gcd n m
[PROOFSTEP]
rw [add_comm, gcd_add_self_left]
[GOAL]
m n : ℕ
⊢ gcd m (m + n) = gcd m n
[PROOFSTEP]
rw [add_comm, gcd_add_self_right]
[GOAL]
m n : ℕ
⊢ 0 < m → 0 < n → 0 < lcm m n
[PROOFSTEP]
simp_rw [pos_iff_ne_zero]
[GOAL]
m n : ℕ
⊢ m ≠ 0 → n ≠ 0 → lcm m n ≠ 0
[PROOFSTEP]
exact lcm_ne_zero
[GOAL]
m n : ℕ
h : coprime m n
⊢ lcm m n = m * n
[PROOFSTEP]
rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
[GOAL]
m n : ℕ
⊢ coprime m (n + m) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_self_right]
[GOAL]
m n : ℕ
⊢ coprime m (m + n) ↔ coprime m n
[PROOFSTEP]
rw [add_comm, coprime_add_self_right]
[GOAL]
m n : ℕ
⊢ coprime (m + n) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_self_left]
[GOAL]
m n : ℕ
⊢ coprime (m + n) m ↔ coprime n m
[PROOFSTEP]
rw [coprime, coprime, gcd_self_add_left]
[GOAL]
m n k : ℕ
⊢ coprime m (n + k * m) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_right_right]
[GOAL]
m n k : ℕ
⊢ coprime m (n + m * k) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_left_right]
[GOAL]
m n k : ℕ
⊢ coprime m (k * m + n) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_right_add_right]
[GOAL]
m n k : ℕ
⊢ coprime m (m * k + n) ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_left_add_right]
[GOAL]
m n k : ℕ
⊢ coprime (m + k * n) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_right_left]
[GOAL]
m n k : ℕ
⊢ coprime (m + n * k) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_add_mul_left_left]
[GOAL]
m n k : ℕ
⊢ coprime (k * n + m) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_right_add_left]
[GOAL]
m n k : ℕ
⊢ coprime (n * k + m) n ↔ coprime m n
[PROOFSTEP]
rw [coprime, coprime, gcd_mul_left_add_left]
[GOAL]
n : ℕ
hn : 0 < n
a b : ℕ
⊢ coprime (a ^ n) b ↔ coprime a b
[PROOFSTEP]
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne'
[GOAL]
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ succ n) b ↔ coprime a b
[PROOFSTEP]
rw [pow_succ, Nat.coprime_mul_iff_left]
[GOAL]
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ n) b ∧ coprime a b ↔ coprime a b
[PROOFSTEP]
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩
[GOAL]
n : ℕ
hn : 0 < n
a b : ℕ
⊢ coprime a (b ^ n) ↔ coprime a b
[PROOFSTEP]
rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
[GOAL]
⊢ ¬coprime 0 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ coprime 1 n ↔ True
[PROOFSTEP]
simp [coprime]
[GOAL]
n : ℕ
⊢ coprime n 1 ↔ True
[PROOFSTEP]
simp [coprime]
[GOAL]
a b c : ℕ
hac : coprime a c
b_dvd_c : b ∣ c
⊢ gcd (a * b) c = b
[PROOFSTEP]
rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
[GOAL]
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd (a * b) (d * b) = b
[PROOFSTEP]
rw [gcd_mul_right]
[GOAL]
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d * b = b
[PROOFSTEP]
convert one_mul b
[GOAL]
case h.e'_2.h.e'_5
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d = 1
[PROOFSTEP]
exact coprime.coprime_mul_right_right hac
[GOAL]
m n k : ℕ
H : k ∣ m * n
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
cases h0 : gcd k m
[GOAL]
case zero
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
case succ m n k : ℕ H : k ∣ m * n n✝ : ℕ h0 : gcd k m = succ n✝ ⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case zero =>
  obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
  obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
  exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case zero =>
  obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
  obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
  exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
h0 : gcd k m = zero
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
obtain rfl : k = 0 := eq_zero_of_gcd_eq_zero_left h0
[GOAL]
m n : ℕ
H : 0 ∣ m * n
h0 : gcd 0 m = zero
⊢ { d // 0 = ↑d.fst * ↑d.snd }
[PROOFSTEP]
obtain rfl : m = 0 := eq_zero_of_gcd_eq_zero_right h0
[GOAL]
n : ℕ
H : 0 ∣ 0 * n
h0 : gcd 0 0 = zero
⊢ { d // 0 = ↑d.fst * ↑d.snd }
[PROOFSTEP]
exact ⟨⟨⟨0, dvd_refl 0⟩, ⟨n, dvd_refl n⟩⟩, (zero_mul n).symm⟩
[GOAL]
case succ
m n k : ℕ
H : k ∣ m * n
n✝ : ℕ
h0 : gcd k m = succ n✝
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case succ tmp =>
  have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _; clear h0 tmp
  have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
  refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
  apply Nat.dvd_of_mul_dvd_mul_left hpos
  rw [hd, ← gcd_mul_right]
  exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
case succ tmp =>
  have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _; clear h0 tmp
  have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
  refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
  apply Nat.dvd_of_mul_dvd_mul_left hpos
  rw [hd, ← gcd_mul_right]
  exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
have hpos : 0 < gcd k m := h0.symm ▸ Nat.zero_lt_succ _
[GOAL]
m n k : ℕ
H : k ∣ m * n
tmp : ℕ
h0 : gcd k m = succ tmp
hpos : 0 < gcd k m
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
clear h0 tmp
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ { d // k = ↑d.fst * ↑d.snd }
[PROOFSTEP]
refine' ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, _⟩⟩, hd.symm⟩
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ k / gcd k m ∣ n
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_left hpos
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ gcd k m * (k / gcd k m) ∣ gcd k m * n
[PROOFSTEP]
rw [hd, ← gcd_mul_right]
[GOAL]
m n k : ℕ
H : k ∣ m * n
hpos : 0 < gcd k m
hd : gcd k m * (k / gcd k m) = k
⊢ k ∣ gcd (k * n) (m * n)
[PROOFSTEP]
exact dvd_gcd (dvd_mul_right _ _) H
[GOAL]
x m n : ℕ
⊢ x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
constructor
[GOAL]
case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
intro h
[GOAL]
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
[PROOFSTEP]
obtain ⟨⟨⟨y, hy⟩, ⟨z, hz⟩⟩, rfl⟩ := prod_dvd_and_dvd_of_dvd_prod h
[GOAL]
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h :
  ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
      ↑({ val := y, property := hy }, { val := z, property := hz }).snd ∣
    m * n
⊢ ∃ y_1 z_1,
    y_1 ∣ m ∧
      z_1 ∣ n ∧
        y_1 * z_1 =
          ↑({ val := y, property := hy }, { val := z, property := hz }).fst *
            ↑({ val := y, property := hy }, { val := z, property := hz }).snd
[PROOFSTEP]
exact ⟨y, z, hy, hz, rfl⟩
[GOAL]
case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n
[PROOFSTEP]
rintro ⟨y, z, hy, hz, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n
[PROOFSTEP]
exact mul_dvd_mul hy hz
[GOAL]
a b n : ℕ
n0 : 0 < n
⊢ a ^ n ∣ b ^ n ↔ a ∣ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => pow_dvd_pow_of_dvd h _⟩
[GOAL]
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
⊢ a ∣ b
[PROOFSTEP]
cases' Nat.eq_zero_or_pos (gcd a b) with g0 g0
[GOAL]
case inl
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b = 0
⊢ a ∣ b
[PROOFSTEP]
simp [eq_zero_of_gcd_eq_zero_right g0]
[GOAL]
case inr
a b n : ℕ
n0 : 0 < n
h : a ^ n ∣ b ^ n
g0 : gcd a b > 0
⊢ a ∣ b
[PROOFSTEP]
rcases exists_coprime' g0 with ⟨g, a', b', g0', co, rfl, rfl⟩
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
[PROOFSTEP]
rw [mul_pow, mul_pow] at h 
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : gcd (a' * g) (b' * g) > 0
⊢ a' * g ∣ b' * g
[PROOFSTEP]
replace h := Nat.dvd_of_mul_dvd_mul_right (pow_pos g0' _) h
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g
[PROOFSTEP]
have := pow_dvd_pow a' n0
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g
[PROOFSTEP]
rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this 
[GOAL]
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : 0 < n
g : ℕ
a' b' : ℕ
g0' : 0 < g
co : coprime a' b'
g0 : gcd (a' * g) (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g
[PROOFSTEP]
simp [eq_one_of_dvd_one this]
[GOAL]
a b k : ℕ
h_ab_coprime : coprime a b
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
[PROOFSTEP]
rw [coprime_iff_gcd_eq_one] at h_ab_coprime 
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1
[PROOFSTEP]
have h1 := dvd_gcd hka hkb
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ gcd a b
⊢ k = 1
[PROOFSTEP]
rw [h_ab_coprime] at h1 
[GOAL]
a b k : ℕ
h_ab_coprime : gcd a b = 1
hka : k ∣ a
hkb : k ∣ b
h1 : k ∣ 1
⊢ k = 1
[PROOFSTEP]
exact Nat.dvd_one.mp h1
[GOAL]
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n
[PROOFSTEP]
intro h
[GOAL]
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
[PROOFSTEP]
obtain ⟨x, rfl⟩ : n ∣ a :=
  cop.symm.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
[GOAL]
case intro
m n b : ℕ
cop : coprime m n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False
[PROOFSTEP]
obtain ⟨y, rfl⟩ : m ∣ b :=
  cop.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
[PROOFSTEP]
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb 
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
[PROOFSTEP]
refine' mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) _)
[GOAL]
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
[PROOFSTEP]
rw [← mul_assoc, ← h, add_mul, add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
