/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-/
import Std.Data.Nat.Lemmas

/-!
# Definitions and properties of `gcd`, `lcm`, and `coprime`

-/

namespace Nat

theorem gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = gcd: Nat → Nat → Nat
gcd (n: Nat
n % m: Nat
m) m: Nat
m :=
  match m: Nat
m with
  | 0: Nat
0 => by
Goals accomplished! 🐙 m, n: Nat

gcd 0 n = gcd (n % 0) 0have := (mod_zero: ∀ (a : Nat), a % 0 = a
mod_zero n: Nat
n).symm: ∀ {α : Sort ?u.189} {a b : α}, a = b → b = a
symmm, n: Nat

this: n = n % 0

gcd 0 n = gcd (n % 0) 0;m, n: Nat

this: n = n % 0

gcd 0 n = gcd (n % 0) 0 m, n: Nat

gcd 0 n = gcd (n % 0) 0rwa [m, n: Nat

this: n = n % 0

gcd 0 n = gcd (n % 0) 0gcd_zero_right: ∀ (n : Nat), gcd n 0 = n
gcd_zero_rightm, n: Nat

this: n = n % 0

gcd 0 n = n % 0]m, n: Nat

this: n = n % 0

gcd 0 n = n % 0
  | _: Nat
_ + 1 => by
Goals accomplished! 🐙 m, n, n✝: Nat

gcd (n✝ + 1) n = gcd (n % (n✝ + 1)) (n✝ + 1)simp [gcd_succ: ∀ (x y : Nat), gcd (succ x) y = gcd (y % succ x) (succ x)
gcd_succ]
Goals accomplished! 🐙

@[elab_as_elim] theorem gcd.induction: ∀ {P : Nat → Nat → Prop} (m n : Nat), (∀ (n : Nat), P 0 n) → (∀ (m n : Nat), 0 < m → P (n % m) m → P m n) → P m n
gcd.induction {P: Nat → Nat → Prop
P : Nat: Type
Nat → Nat: Type
Nat → Prop: Type
Prop} (m: Nat
m n: Nat
n : Nat: Type
Nat)
    (H0: ∀ (n : Nat), P 0 n
H0 : ∀n: ?m.327
n, P: Nat → Nat → Prop
P 0: ?m.331
0 n: ?m.327
n) (H1: ∀ (m n : Nat), 0 < m → P (n % m) m → P m n
H1 : ∀ m: ?m.342
m n: ?m.345
n, 0: ?m.351
0 < m: ?m.342
m → P: Nat → Nat → Prop
P (n: ?m.345
n % m: ?m.342
m) m: ?m.342
m → P: Nat → Nat → Prop
P m: ?m.342
m n: ?m.345
n) : P: Nat → Nat → Prop
P m: Nat
m n: Nat
n :=
  Nat.strongInductionOn: ∀ {motive : Nat → Sort ?u.455} (n : Nat), (∀ (n : Nat), (∀ (m : Nat), m < n → motive m) → motive n) → motive n
Nat.strongInductionOn (motive := fun m: ?m.457
m => ∀ n: ?m.460
n, P: Nat → Nat → Prop
P m: ?m.457
m n: ?m.460
n) m: Nat
m
    (fun
    | 0: Nat
0, _ => H0: ∀ (n : Nat), P 0 n
H0
    | _+1, IH: ∀ (m : Nat), m < n✝ + 1 → (fun m => ∀ (n : Nat), P m n) m
IH => fun _: ?m.615
_ => H1: ∀ (m n : Nat), 0 < m → P (n % m) m → P m n
H1 _: Nat
_ _: Nat
_ (succ_pos: ∀ (n : Nat), 0 < succ n
succ_pos _: Nat
_) (IH: ∀ (m : Nat), m < n✝ + 1 → (fun m => ∀ (n : Nat), P m n) m
IH _: Nat
_ (mod_lt: ∀ (x : Nat) {y : Nat}, y > 0 → x % y < y
mod_lt _: Nat
_ (succ_pos: ∀ (n : Nat), 0 < succ n
succ_pos _: Nat
_)) _: Nat
_) )
    n: Nat
n

/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
def lcm: Nat → Nat → Nat
lcm (m: Nat
m n: Nat
n : Nat: Type
Nat) : Nat: Type
Nat := m: Nat
m * n: Nat
n / gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n

/-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/
@[reducible] def coprime: Nat → Nat → Prop
coprime (m: Nat
m n: Nat
n : Nat: Type
Nat) : Prop: Type
Prop := gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = 1: ?m.1158
1

---

theorem gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd (m: Nat
m n: Nat
n : Nat: Type
Nat) : (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ m: Nat
m) ∧ (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ n: Nat
n) := by
Goals accomplished! 🐙
  m, n: Nat

gcd m n ∣ m ∧ gcd m n ∣ ninduction m: Nat
m, n: Nat
n using gcd.induction: ∀ {P : Nat → Nat → Prop} (m n : Nat), (∀ (n : Nat), P 0 n) → (∀ (m n : Nat), 0 < m → P (n % m) m → P m n) → P m n
gcd.induction with
  m, n: Nat

gcd m n ∣ m ∧ gcd m n ∣ n| H0 n: Nat
n => n: Nat

H0gcd 0 n ∣ 0 ∧ gcd 0 n ∣ nrw [n: Nat

H0gcd 0 n ∣ 0 ∧ gcd 0 n ∣ ngcd_zero_left: ∀ (y : Nat), gcd 0 y = y
gcd_zero_leftn: Nat

H0n ∣ 0 ∧ n ∣ n]n: Nat

H0n ∣ 0 ∧ n ∣ n;n: Nat

H0n ∣ 0 ∧ n ∣ n n: Nat

H0gcd 0 n ∣ 0 ∧ gcd 0 n ∣ nexact ⟨Nat.dvd_zero: ∀ (a : Nat), a ∣ 0
Nat.dvd_zero n: Nat
n, Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl n: Nat
n⟩
Goals accomplished! 🐙
  m, n: Nat

gcd m n ∣ m ∧ gcd m n ∣ n| H1 m: Nat
m n: Nat
n _: 0 < m
_ IH: ?m.1213 (n % m) m
IH => m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ nrw [m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ n← gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_recm, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ n]m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ n at IH: ?m.1213 (n % m) m
IHm, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ n;m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ n m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m

H1gcd m n ∣ m ∧ gcd m n ∣ nexact ⟨IH: gcd m n ∣ n % m ∧ gcd m n ∣ m
IH.2: ∀ {a b : Prop}, a ∧ b → b
2, (dvd_mod_iff: ∀ {k m n : Nat}, k ∣ n → (k ∣ m % n ↔ k ∣ m)
dvd_mod_iff IH: gcd m n ∣ n % m ∧ gcd m n ∣ m
IH.2: ∀ {a b : Prop}, a ∧ b → b
2).1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 IH: gcd m n ∣ n % m ∧ gcd m n ∣ m
IH.1: ∀ {a b : Prop}, a ∧ b → a
1⟩
Goals accomplished! 🐙

theorem gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ m: Nat
m := (gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd m: Nat
m n: Nat
n).left: ∀ {a b : Prop}, a ∧ b → a
left

theorem gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ n: Nat
n := (gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd m: Nat
m n: Nat
n).right: ∀ {a b : Prop}, a ∧ b → b
right

theorem gcd_le_left: ∀ {m : Nat} (n : Nat), 0 < m → gcd m n ≤ m
gcd_le_left (n: ?m.1383
n) (h: 0 < m
h : 0: ?m.1388
0 < m: ?m.1380
m) : gcd: Nat → Nat → Nat
gcd m: ?m.1380
m n: ?m.1383
n ≤ m: ?m.1380
m := le_of_dvd: ∀ {m n : Nat}, 0 < n → m ∣ n → m ≤ n
le_of_dvd h: 0 < m
h <| gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n

theorem gcd_le_right: ∀ {m : Nat} (n : Nat), 0 < n → gcd m n ≤ n
gcd_le_right (n: ?m.1513
n) (h: 0 < n
h : 0: ?m.1518
0 < n: ?m.1513
n) : gcd: Nat → Nat → Nat
gcd m: ?m.1510
m n: ?m.1513
n ≤ n: ?m.1513
n := le_of_dvd: ∀ {m n : Nat}, 0 < n → m ∣ n → m ≤ n
le_of_dvd h: 0 < n
h <| gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n

theorem dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd : k: ?m.1599
k ∣ m: ?m.1609
m → k: ?m.1599
k ∣ n: ?m.1629
n → k: ?m.1599
k ∣ gcd: Nat → Nat → Nat
gcd m: ?m.1609
m n: ?m.1629
n := by
Goals accomplished! 🐙
  k, m, n: Nat

k ∣ m → k ∣ n → k ∣ gcd m ninduction m: Nat
m, n: Nat
n using gcd.induction: ∀ {P : Nat → Nat → Prop} (m n : Nat), (∀ (n : Nat), P 0 n) → (∀ (m n : Nat), 0 < m → P (n % m) m → P m n) → P m n
gcd.induction with k, m, n: Nat

k ∣ m → k ∣ n → k ∣ gcd m nintro km: k ∣ 0
km kn: k ∣ m
knk, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd n m
  k, m, n: Nat

k ∣ m → k ∣ n → k ∣ gcd m n| H0 n: Nat
n => k, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ gcd 0 nrw [k, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ gcd 0 ngcd_zero_left: ∀ (y : Nat), gcd 0 y = y
gcd_zero_leftk, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ n]k, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ n;k, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ n k, n: Nat

km: k ∣ 0

kn: k ∣ n

H0k ∣ gcd 0 nexact kn: k ∣ n
kn
Goals accomplished! 🐙
  k, m, n: Nat

k ∣ m → k ∣ n → k ∣ gcd m n| H1 n: Nat
n m: Nat
m _: 0 < n
_ IH: ?m.1685 (m % n) n
IH => k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd n mrw [k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd n mgcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_reck, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd (m % n) n]k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd (m % n) n;k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd (m % n) n k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m

H1k ∣ gcd n mexact IH: ?m.1685 (m % n) n
IH ((dvd_mod_iff: ∀ {k m n : Nat}, k ∣ n → (k ∣ m % n ↔ k ∣ m)
dvd_mod_iff km: k ∣ n
km).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 kn: k ∣ m
kn) km: k ∣ n
km
Goals accomplished! 🐙

theorem dvd_gcd_iff: ∀ {k : Nat} {m n : Nat}, k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n
dvd_gcd_iff : k: ?m.1788
k ∣ gcd: Nat → Nat → Nat
gcd m: ?m.1795
m n: ?m.1802
n ↔ k: ?m.1788
k ∣ m: ?m.1795
m ∧ k: ?m.1788
k ∣ n: ?m.1802
n :=
  ⟨fun h: ?m.1829
h => let ⟨h₁: gcd m n ∣ m
h₁, h₂: gcd m n ∣ n
h₂⟩ := gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd m: Nat
m n: Nat
n; ⟨Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans h: ?m.1829
h h₁: gcd m n ∣ m
h₁, Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans h: ?m.1829
h h₂: gcd m n ∣ n
h₂⟩,
   fun ⟨h₁: k ∣ m
h₁, h₂: k ∣ n
h₂⟩ => dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd h₁: k ∣ m
h₁ h₂: k ∣ n
h₂⟩

theorem gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m :=
  dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
    (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n) (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n))
    (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right n: Nat
n m: Nat
m) (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left n: Nat
n m: Nat
m))

theorem gcd_eq_left_iff_dvd: ∀ {m n : Nat}, m ∣ n ↔ gcd m n = m
gcd_eq_left_iff_dvd : m: ?m.2071
m ∣ n: ?m.2078
n ↔ gcd: Nat → Nat → Nat
gcd m: ?m.2071
m n: ?m.2078
n = m: ?m.2071
m :=
  ⟨fun h: ?m.2105
h => by
Goals accomplished! 🐙 m, n: Nat

h: m ∣ n

gcd m n = mrw [m, n: Nat

h: m ∣ n

gcd m n = mgcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec,m, n: Nat

h: m ∣ n

gcd (n % m) m = m m, n: Nat

h: m ∣ n

gcd m n = mmod_eq_zero_of_dvd: ∀ {m n : Nat}, m ∣ n → n % m = 0
mod_eq_zero_of_dvd h: m ∣ n
h,m, n: Nat

h: m ∣ n

gcd 0 m = m m, n: Nat

h: m ∣ n

gcd m n = mgcd_zero_left: ∀ (y : Nat), gcd 0 y = y
gcd_zero_leftm, n: Nat

h: m ∣ n

m = m]
Goals accomplished! 🐙,
   fun h: ?m.2112
h => h: ?m.2112
h ▸ gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n⟩

theorem gcd_eq_right_iff_dvd: ∀ {m n : Nat}, m ∣ n ↔ gcd n m = m
gcd_eq_right_iff_dvd : m: ?m.2165
m ∣ n: ?m.2172
n ↔ gcd: Nat → Nat → Nat
gcd n: ?m.2172
n m: ?m.2165
m = m: ?m.2165
m := by
Goals accomplished! 🐙
  m, n: Nat

m ∣ n ↔ gcd n m = mrw [m, n: Nat

m ∣ n ↔ gcd n m = mgcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_commm, n: Nat

m ∣ n ↔ gcd m n = m]m, n: Nat

m ∣ n ↔ gcd m n = m;m, n: Nat

m ∣ n ↔ gcd m n = m m, n: Nat

m ∣ n ↔ gcd n m = mexact gcd_eq_left_iff_dvd: ∀ {m n : Nat}, m ∣ n ↔ gcd m n = m
gcd_eq_left_iff_dvd
Goals accomplished! 🐙

theorem gcd_assoc: ∀ (m n k : Nat), gcd (gcd m n) k = gcd m (gcd n k)
gcd_assoc (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) k: Nat
k = gcd: Nat → Nat → Nat
gcd m: Nat
m (gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k) :=
  dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
    (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
      (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) k: Nat
k) (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n))
      (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) k: Nat
k) (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n))
        (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) k: Nat
k)))
    (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
      (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m (gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k))
        (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m (gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k)) (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left n: Nat
n k: Nat
k)))
      (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m (gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k)) (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right n: Nat
n k: Nat
k)))

@[simp] theorem gcd_one_right: ∀ (n : Nat), gcd n 1 = 1
gcd_one_right (n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd n: Nat
n 1: ?m.2280
1 = 1: ?m.2289
1 := (gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm n: Nat
n 1: ?m.2306
1).trans: ∀ {α : Sort ?u.2308} {a b c : α}, a = b → b = c → a = c
trans (gcd_one_left: ∀ (n : Nat), gcd 1 n = 1
gcd_one_left n: Nat
n)

theorem gcd_mul_left: ∀ (m n k : Nat), gcd (m * n) (m * k) = m * gcd n k
gcd_mul_left (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (m: Nat
m * n: Nat
n) (m: Nat
m * k: Nat
k) = m: Nat
m * gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k := by
Goals accomplished! 🐙
  m, n, k: Nat

gcd (m * n) (m * k) = m * gcd n kinduction n: Nat
n, k: Nat
k using gcd.induction: ∀ {P : Nat → Nat → Prop} (m n : Nat), (∀ (n : Nat), P 0 n) → (∀ (m n : Nat), 0 < m → P (n % m) m → P m n) → P m n
gcd.induction with
  m, n, k: Nat

gcd (m * n) (m * k) = m * gcd n k| H0 k: Nat
k => m, k: Nat

H0gcd (m * 0) (m * k) = m * gcd 0 ksimp
Goals accomplished! 🐙
  m, n, k: Nat

gcd (m * n) (m * k) = m * gcd n k| H1 n: Nat
n k: Nat
k _: 0 < n
_ IH: ?m.2444 (k % n) n
IH => m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n krwa [m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n k← mul_mod_mul_left: ∀ (z x y : Nat), z * x % (z * y) = z * (x % y)
mul_mod_mul_left,m, n, k: Nat

a✝: 0 < n

IH: gcd (m * k % (m * n)) (m * n) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n k m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n k← gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec,m, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n k m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n

H1gcd (m * n) (m * k) = m * gcd n k← gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_recm, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd n k

H1gcd (m * n) (m * k) = m * gcd n k]m, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd n k

H1gcd (m * n) (m * k) = m * gcd n k at IH: gcd (m * k % (m * n)) (m * n) = m * gcd (k % n) n
IH
Goals accomplished! 🐙

theorem gcd_mul_right: ∀ (m n k : Nat), gcd (m * n) (k * n) = gcd m k * n
gcd_mul_right (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (m: Nat
m * n: Nat
n) (k: Nat
k * n: Nat
n) = gcd: Nat → Nat → Nat
gcd m: Nat
m k: Nat
k * n: Nat
n := by
Goals accomplished! 🐙
  m, n, k: Nat

gcd (m * n) (k * n) = gcd m k * nrw [m, n, k: Nat

gcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm m: Nat
m n: Nat
n,m, n, k: Nat

gcd (n * m) (k * n) = gcd m k * n m, n, k: Nat

gcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm k: Nat
k n: Nat
n,m, n, k: Nat

gcd (n * m) (n * k) = gcd m k * n m, n, k: Nat

gcd (m * n) (k * n) = gcd m k * nNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm (gcd: Nat → Nat → Nat
gcd m: Nat
m k: Nat
k) n: Nat
n,m, n, k: Nat

gcd (n * m) (n * k) = n * gcd m k m, n, k: Nat

gcd (m * n) (k * n) = gcd m k * ngcd_mul_left: ∀ (m n k : Nat), gcd (m * n) (m * k) = m * gcd n k
gcd_mul_leftm, n, k: Nat

n * gcd m k = n * gcd m k]
Goals accomplished! 🐙

theorem gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
gcd_pos_of_pos_left {m: Nat
m : Nat: Type
Nat} (n: Nat
n : Nat: Type
Nat) (mpos: 0 < m
mpos : 0: ?m.2747
0 < m: Nat
m) : 0: ?m.2775
0 < gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n :=
  pos_of_dvd_of_pos: ∀ {m n : Nat}, m ∣ n → 0 < n → 0 < m
pos_of_dvd_of_pos (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n) mpos: 0 < m
mpos

theorem gcd_pos_of_pos_right: ∀ (m : Nat) {n : Nat}, 0 < n → 0 < gcd m n
gcd_pos_of_pos_right (m: Nat
m : Nat: Type
Nat) {n: Nat
n : Nat: Type
Nat} (npos: 0 < n
npos : 0: ?m.2818
0 < n: Nat
n) : 0: ?m.2846
0 < gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n :=
  pos_of_dvd_of_pos: ∀ {m n : Nat}, m ∣ n → 0 < n → 0 < m
pos_of_dvd_of_pos (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n) npos: 0 < n
npos

theorem div_gcd_pos_of_pos_left: ∀ {a : Nat} (b : Nat), 0 < a → 0 < a / gcd a b
div_gcd_pos_of_pos_left (b: Nat
b : Nat: Type
Nat) (h: 0 < a
h : 0: ?m.2906
0 < a: ?m.2899
a) : 0: ?m.2949
0 < a: ?m.2899
a / a: ?m.2899
a.gcd: Nat → Nat → Nat
gcd b: Nat
b :=
  (Nat.le_div_iff_mul_le: ∀ {k x y : Nat}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
Nat.gcd_pos_of_pos_left _: Nat
_ h: 0 < a
h).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (Nat.one_mul: ∀ (n : Nat), 1 * n = n
Nat.one_mul _: Nat
_ ▸ Nat.gcd_le_left: ∀ {m : Nat} (n : Nat), 0 < m → gcd m n ≤ m
Nat.gcd_le_left _: Nat
_ h: 0 < a
h)

theorem div_gcd_pos_of_pos_right: ∀ {b : Nat} (a : Nat), 0 < b → 0 < b / gcd a b
div_gcd_pos_of_pos_right (a: Nat
a : Nat: Type
Nat) (h: 0 < b
h : 0: ?m.3173
0 < b: ?m.3166
b) : 0: ?m.3216
0 < b: ?m.3166
b / a: Nat
a.gcd: Nat → Nat → Nat
gcd b: ?m.3166
b :=
  (Nat.le_div_iff_mul_le: ∀ {k x y : Nat}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right: ∀ (m : Nat) {n : Nat}, 0 < n → 0 < gcd m n
Nat.gcd_pos_of_pos_right _: Nat
_ h: 0 < b
h).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (Nat.one_mul: ∀ (n : Nat), 1 * n = n
Nat.one_mul _: Nat
_ ▸ Nat.gcd_le_right: ∀ {m : Nat} (n : Nat), 0 < n → gcd m n ≤ n
Nat.gcd_le_right _: Nat
_ h: 0 < b
h)

theorem eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left {m: Nat
m n: Nat
n : Nat: Type
Nat} (H: gcd m n = 0
H : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = 0: ?m.3345
0) : m: Nat
m = 0: ?m.3367
0 :=
  match eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos m: Nat
m with
  | .inl: ∀ {a b : Prop}, a → a ∨ b
.inl H0: m = 0
H0 => H0: m = 0
H0
  | .inr: ∀ {a b : Prop}, b → a ∨ b
.inr H1: m > 0
H1 => absurd: ∀ {a : Prop} {b : Sort ?u.3408}, a → ¬a → b
absurd (Eq.symm: ∀ {α : Sort ?u.3411} {a b : α}, a = b → b = a
Eq.symm H: gcd m n = 0
H) (ne_of_lt: ∀ {a b : Nat}, a < b → a ≠ b
ne_of_lt (gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
gcd_pos_of_pos_left _: Nat
_ H1: m > 0
H1))

theorem eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right {m: Nat
m n: Nat
n : Nat: Type
Nat} (H: gcd m n = 0
H : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = 0: ?m.3511
0) : n: Nat
n = 0: ?m.3533
0 := by
Goals accomplished! 🐙
  m, n: Nat

H: gcd m n = 0

n = 0rw [m, n: Nat

H: gcd m n = 0

n = 0gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_commm, n: Nat

H: gcd n m = 0

n = 0]m, n: Nat

H: gcd n m = 0

n = 0 at H: gcd m n = 0
Hm, n: Nat

H: gcd n m = 0

n = 0
  m, n: Nat

H: gcd m n = 0

n = 0exact eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left H: gcd n m = 0
H
Goals accomplished! 🐙

theorem gcd_ne_zero_left: ∀ {m n : Nat}, m ≠ 0 → gcd m n ≠ 0
gcd_ne_zero_left : m: ?m.3590
m ≠ 0: ?m.3617
0 → gcd: Nat → Nat → Nat
gcd m: ?m.3590
m n: ?m.3610
n ≠ 0: ?m.3630
0 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left

theorem gcd_ne_zero_right: ∀ {n m : Nat}, n ≠ 0 → gcd m n ≠ 0
gcd_ne_zero_right : n: ?m.3673
n ≠ 0: ?m.3700
0 → gcd: Nat → Nat → Nat
gcd m: ?m.3693
m n: ?m.3673
n ≠ 0: ?m.3713
0 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right

theorem gcd_div: ∀ {m n k : Nat}, k ∣ m → k ∣ n → gcd (m / k) (n / k) = gcd m n / k
gcd_div {m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat} (H1: k ∣ m
H1 : k: Nat
k ∣ m: Nat
m) (H2: k ∣ n
H2 : k: Nat
k ∣ n: Nat
n) :
    gcd: Nat → Nat → Nat
gcd (m: Nat
m / k: Nat
k) (n: Nat
n / k: Nat
k) = gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n / k: Nat
k :=
  match eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos k: Nat
k with
  | .inl: ∀ {a b : Prop}, a → a ∨ b
.inl H0: k = 0
H0 => by
Goals accomplished! 🐙 m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H0: k = 0

gcd (m / k) (n / k) = gcd m n / ksimp [H0: k = 0
H0]
Goals accomplished! 🐙
  | .inr: ∀ {a b : Prop}, b → a ∨ b
.inr H3: k > 0
H3 => by
Goals accomplished! 🐙
    m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) = gcd m n / kapply Nat.eq_of_mul_eq_mul_right: ∀ {n m k : Nat}, 0 < m → n * m = k * m → n = k
Nat.eq_of_mul_eq_mul_right H3: k > 0
H3m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n / k * k
    m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) = gcd m n / krw [m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ∀ {n m : Nat}, n ∣ m → m / n * n = m
Nat.div_mul_cancel (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd H1: k ∣ m
H1 H2: k ∣ n
H2),m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n / k * k← gcd_mul_right: ∀ (m n k : Nat), gcd (m * n) (k * n) = gcd m k * n
gcd_mul_right,m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k * k) (n / k * k) = gcd m n
        m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ∀ {n m : Nat}, n ∣ m → m / n * n = m
Nat.div_mul_cancel H1: k ∣ m
H1,m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd m (n / k * k) = gcd m n m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd (m / k) (n / k) * k = gcd m n / k * kNat.div_mul_cancel: ∀ {n m : Nat}, n ∣ m → m / n * n = m
Nat.div_mul_cancel H2: k ∣ n
H2m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0

gcd m n = gcd m n]
Goals accomplished! 🐙

theorem gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left {m: Nat
m k: Nat
k : Nat: Type
Nat} (n: Nat
n : Nat: Type
Nat) (H: m ∣ k
H : m: Nat
m ∣ k: Nat
k) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ gcd: Nat → Nat → Nat
gcd k: Nat
k n: Nat
n :=
  dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n) H: m ∣ k
H) (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right m: Nat
m n: Nat
n)

theorem gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right {m: Nat
m k: Nat
k : Nat: Type
Nat} (n: Nat
n : Nat: Type
Nat) (H: m ∣ k
H : m: Nat
m ∣ k: Nat
k) : gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m ∣ gcd: Nat → Nat → Nat
gcd n: Nat
n k: Nat
k :=
  dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left n: Nat
n m: Nat
m) (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right n: Nat
n m: Nat
m) H: m ∣ k
H)

theorem gcd_dvd_gcd_mul_left: ∀ (m n k : Nat), gcd m n ∣ gcd (k * m) n
gcd_dvd_gcd_mul_left (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ gcd: Nat → Nat → Nat
gcd (k: Nat
k * m: Nat
m) n: Nat
n :=
  gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left _: Nat
_ (Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left _: Nat
_ _: Nat
_)

theorem gcd_dvd_gcd_mul_right: ∀ (m n k : Nat), gcd m n ∣ gcd (m * k) n
gcd_dvd_gcd_mul_right (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ gcd: Nat → Nat → Nat
gcd (m: Nat
m * k: Nat
k) n: Nat
n :=
  gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left _: Nat
_ (Nat.dvd_mul_right: ∀ (a b : Nat), a ∣ a * b
Nat.dvd_mul_right _: Nat
_ _: Nat
_)

theorem gcd_dvd_gcd_mul_left_right: ∀ (m n k : Nat), gcd m n ∣ gcd m (k * n)
gcd_dvd_gcd_mul_left_right (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ gcd: Nat → Nat → Nat
gcd m: Nat
m (k: Nat
k * n: Nat
n) :=
  gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right _: Nat
_ (Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left _: Nat
_ _: Nat
_)

theorem gcd_dvd_gcd_mul_right_right: ∀ (m n k : Nat), gcd m n ∣ gcd m (n * k)
gcd_dvd_gcd_mul_right_right (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n ∣ gcd: Nat → Nat → Nat
gcd m: Nat
m (n: Nat
n * k: Nat
k) :=
  gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right _: Nat
_ (Nat.dvd_mul_right: ∀ (a b : Nat), a ∣ a * b
Nat.dvd_mul_right _: Nat
_ _: Nat
_)

theorem gcd_eq_left: ∀ {m n : Nat}, m ∣ n → gcd m n = m
gcd_eq_left {m: Nat
m n: Nat
n : Nat: Type
Nat} (H: m ∣ n
H : m: Nat
m ∣ n: Nat
n) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = m: Nat
m :=
  dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left _: Nat
_ _: Nat
_) (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl _: Nat
_) H: m ∣ n
H)

theorem gcd_eq_right: ∀ {m n : Nat}, n ∣ m → gcd m n = n
gcd_eq_right {m: Nat
m n: Nat
n : Nat: Type
Nat} (H: n ∣ m
H : n: Nat
n ∣ m: Nat
m) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n = n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

H: n ∣ m

gcd m n = nrw [m, n: Nat

H: n ∣ m

gcd m n = ngcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm,m, n: Nat

H: n ∣ m

gcd n m = n m, n: Nat

H: n ∣ m

gcd m n = ngcd_eq_left: ∀ {m n : Nat}, m ∣ n → gcd m n = m
gcd_eq_left H: n ∣ m
Hm, n: Nat

H: n ∣ m

n = n]
Goals accomplished! 🐙

@[simp] theorem gcd_mul_left_left: ∀ (m n : Nat), gcd (m * n) n = n
gcd_mul_left_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (m: Nat
m * n: Nat
n) n: Nat
n = n: Nat
n :=
  dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right _: Nat
_ _: Nat
_) (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left _: Nat
_ _: Nat
_) (Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl _: Nat
_))

@[simp] theorem gcd_mul_left_right: ∀ (m n : Nat), gcd n (m * n) = n
gcd_mul_left_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd n: Nat
n (m: Nat
m * n: Nat
n) = n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

gcd n (m * n) = nrw [m, n: Nat

gcd n (m * n) = ngcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm,m, n: Nat

gcd (m * n) n = n m, n: Nat

gcd n (m * n) = ngcd_mul_left_left: ∀ (m n : Nat), gcd (m * n) n = n
gcd_mul_left_leftm, n: Nat

n = n]
Goals accomplished! 🐙

@[simp] theorem gcd_mul_right_left: ∀ (m n : Nat), gcd (n * m) n = n
gcd_mul_right_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (n: Nat
n * m: Nat
m) n: Nat
n = n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

gcd (n * m) n = nrw [m, n: Nat

gcd (n * m) n = nNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm,m, n: Nat

gcd (m * n) n = n m, n: Nat

gcd (n * m) n = ngcd_mul_left_left: ∀ (m n : Nat), gcd (m * n) n = n
gcd_mul_left_leftm, n: Nat

n = n]
Goals accomplished! 🐙

@[simp] theorem gcd_mul_right_right: ∀ (m n : Nat), gcd n (n * m) = n
gcd_mul_right_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd n: Nat
n (n: Nat
n * m: Nat
m) = n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

gcd n (n * m) = nrw [m, n: Nat

gcd n (n * m) = ngcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm,m, n: Nat

gcd (n * m) n = n m, n: Nat

gcd n (n * m) = ngcd_mul_right_left: ∀ (m n : Nat), gcd (n * m) n = n
gcd_mul_right_leftm, n: Nat

n = n]
Goals accomplished! 🐙

@[simp] theorem gcd_gcd_self_right_left: ∀ (m n : Nat), gcd m (gcd m n) = gcd m n
gcd_gcd_self_right_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) = gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n :=
  dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm (gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right _: Nat
_ _: Nat
_) (dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left _: Nat
_ _: Nat
_) (Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl _: Nat
_))

@[simp] theorem gcd_gcd_self_right_right: ∀ (m n : Nat), gcd m (gcd n m) = gcd n m
gcd_gcd_self_right_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m (gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m) = gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m := by
Goals accomplished! 🐙
  m, n: Nat

gcd m (gcd n m) = gcd n mrw [m, n: Nat

gcd m (gcd n m) = gcd n mgcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm n: Nat
n m: Nat
m,m, n: Nat

gcd m (gcd m n) = gcd m n m, n: Nat

gcd m (gcd n m) = gcd n mgcd_gcd_self_right_left: ∀ (m n : Nat), gcd m (gcd m n) = gcd m n
gcd_gcd_self_right_leftm, n: Nat

gcd m n = gcd m n]
Goals accomplished! 🐙

@[simp] theorem gcd_gcd_self_left_right: ∀ (m n : Nat), gcd (gcd n m) m = gcd n m
gcd_gcd_self_left_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m) m: Nat
m = gcd: Nat → Nat → Nat
gcd n: Nat
n m: Nat
m := by
Goals accomplished! 🐙
  m, n: Nat

gcd (gcd n m) m = gcd n mrw [m, n: Nat

gcd (gcd n m) m = gcd n mgcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm,m, n: Nat

gcd m (gcd n m) = gcd n m m, n: Nat

gcd (gcd n m) m = gcd n mgcd_gcd_self_right_right: ∀ (m n : Nat), gcd m (gcd n m) = gcd n m
gcd_gcd_self_right_rightm, n: Nat

gcd n m = gcd n m]
Goals accomplished! 🐙

@[simp] theorem gcd_gcd_self_left_left: ∀ (m n : Nat), gcd (gcd m n) m = gcd m n
gcd_gcd_self_left_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd (gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n) m: Nat
m = gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

gcd (gcd m n) m = gcd m nrw [m, n: Nat

gcd (gcd m n) m = gcd m ngcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm m: Nat
m n: Nat
n,m, n: Nat

gcd (gcd n m) m = gcd n m m, n: Nat

gcd (gcd m n) m = gcd m ngcd_gcd_self_left_right: ∀ (m n : Nat), gcd (gcd n m) m = gcd n m
gcd_gcd_self_left_rightm, n: Nat

gcd n m = gcd n m]
Goals accomplished! 🐙

theorem gcd_add_mul_self: ∀ (m n k : Nat), gcd m (n + k * m) = gcd m n
gcd_add_mul_self (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m (n: Nat
n + k: Nat
k * m: Nat
m) = gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n := by
Goals accomplished! 🐙
  m, n, k: Nat

gcd m (n + k * m) = gcd m nsimp [gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec m: Nat
m (n: Nat
n + k: Nat
k * m: Nat
m), gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec m: Nat
m n: Nat
n]
Goals accomplished! 🐙

theorem gcd_eq_zero_iff: ∀ {i j : Nat}, gcd i j = 0 ↔ i = 0 ∧ j = 0
gcd_eq_zero_iff {i: Nat
i j: Nat
j : Nat: Type
Nat} : gcd: Nat → Nat → Nat
gcd i: Nat
i j: Nat
j = 0: ?m.5334
0 ↔ i: Nat
i = 0: ?m.5354
0 ∧ j: Nat
j = 0: ?m.5368
0 :=
  ⟨fun h: ?m.5392
h => ⟨eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left h: ?m.5392
h, eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right h: ?m.5392
h⟩,
   fun h: ?m.5414
h => by
Goals accomplished! 🐙 i, j: Nat

h: i = 0 ∧ j = 0

gcd i j = 0simp [h: i = 0 ∧ j = 0
h]
Goals accomplished! 🐙⟩

/-! ### `lcm` -/

theorem lcm_comm: ∀ (m n : Nat), lcm m n = lcm n m
lcm_comm (m: Nat
m n: Nat
n : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n = lcm: Nat → Nat → Nat
lcm n: Nat
n m: Nat
m := by
Goals accomplished! 🐙
  m, n: Nat

lcm m n = lcm n mrw [m, n: Nat

lcm m n = lcm n mlcm: Nat → Nat → Nat
lcm,m, n: Nat

m * n / gcd m n = lcm n m m, n: Nat

lcm m n = lcm n mlcm: Nat → Nat → Nat
lcm,m, n: Nat

m * n / gcd m n = n * m / gcd n m m, n: Nat

lcm m n = lcm n mNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm n: Nat
n m: Nat
m,m, n: Nat

m * n / gcd m n = m * n / gcd n m m, n: Nat

lcm m n = lcm n mgcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm n: Nat
n m: Nat
mm, n: Nat

m * n / gcd m n = m * n / gcd m n]
Goals accomplished! 🐙

@[simp] theorem lcm_zero_left: ∀ (m : Nat), lcm 0 m = 0
lcm_zero_left (m: Nat
m : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm 0: ?m.5514
0 m: Nat
m = 0: ?m.5523
0 := by
Goals accomplished! 🐙 m: Nat

lcm 0 m = 0simp [lcm: Nat → Nat → Nat
lcm]
Goals accomplished! 🐙

@[simp] theorem lcm_zero_right: ∀ (m : Nat), lcm m 0 = 0
lcm_zero_right (m: Nat
m : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm m: Nat
m 0: ?m.5650
0 = 0: ?m.5659
0 := by
Goals accomplished! 🐙 m: Nat

lcm m 0 = 0simp [lcm: Nat → Nat → Nat
lcm]
Goals accomplished! 🐙

@[simp] theorem lcm_one_left: ∀ (m : Nat), lcm 1 m = m
lcm_one_left (m: Nat
m : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm 1: ?m.5782
1 m: Nat
m = m: Nat
m := by
Goals accomplished! 🐙 m: Nat

lcm 1 m = msimp [lcm: Nat → Nat → Nat
lcm]
Goals accomplished! 🐙

@[simp] theorem lcm_one_right: ∀ (m : Nat), lcm m 1 = m
lcm_one_right (m: Nat
m : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm m: Nat
m 1: ?m.5904
1 = m: Nat
m := by
Goals accomplished! 🐙 m: Nat

lcm m 1 = msimp [lcm: Nat → Nat → Nat
lcm]
Goals accomplished! 🐙

@[simp] theorem lcm_self: ∀ (m : Nat), lcm m m = m
lcm_self (m: Nat
m : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm m: Nat
m m: Nat
m = m: Nat
m := by
Goals accomplished! 🐙
  m: Nat

lcm m m = mmatch eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos m: Nat
m with
  m: Nat

lcm m m = m| .inl: ∀ {a b : Prop}, a → a ∨ b
.inl h: m = 0
h =>m: Nat

h: m = 0

lcm m m = m m: Nat

lcm m m = mrw [m: Nat

h: m = 0

lcm m m = mh: m = 0
h,m: Nat

h: m = 0

lcm 0 0 = 0 m: Nat

h: m = 0

lcm m m = mlcm_zero_left: ∀ (m : Nat), lcm 0 m = 0
lcm_zero_leftm: Nat

h: m = 0

0 = 0]
Goals accomplished! 🐙
  m: Nat

lcm m m = m| .inr: ∀ {a b : Prop}, b → a ∨ b
.inr h: m > 0
h =>m: Nat

h: m > 0

lcm m m = m m: Nat

lcm m m = msimp [lcm: Nat → Nat → Nat
lcm, Nat.mul_div_cancel: ∀ (m : Nat) {n : Nat}, 0 < n → m * n / n = m
Nat.mul_div_cancel _: Nat
_ h: m > 0
h]
Goals accomplished! 🐙

theorem dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left (m: Nat
m n: Nat
n : Nat: Type
Nat) : m: Nat
m ∣ lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n :=
  ⟨n: Nat
n / gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n, by
Goals accomplished! 🐙 m, n: Nat

lcm m n = m * (n / gcd m n)rw [m, n: Nat

lcm m n = m * (n / gcd m n)← Nat.mul_div_assoc: ∀ {k n : Nat} (m : Nat), k ∣ n → m * n / k = m * (n / k)
Nat.mul_div_assoc m: Nat
m (Nat.gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
Nat.gcd_dvd_right m: Nat
m n: Nat
n)m, n: Nat

lcm m n = m * n / gcd m n]m, n: Nat

lcm m n = m * n / gcd m n;m, n: Nat

lcm m n = m * n / gcd m n m, n: Nat

lcm m n = m * (n / gcd m n)rfl
Goals accomplished! 🐙⟩

theorem dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right (m: Nat
m n: Nat
n : Nat: Type
Nat) : n: Nat
n ∣ lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n := lcm_comm: ∀ (m n : Nat), lcm m n = lcm n m
lcm_comm n: Nat
n m: Nat
m ▸ dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left n: Nat
n m: Nat
m

theorem gcd_mul_lcm: ∀ (m n : Nat), gcd m n * lcm m n = m * n
gcd_mul_lcm (m: Nat
m n: Nat
n : Nat: Type
Nat) : gcd: Nat → Nat → Nat
gcd m: Nat
m n: Nat
n * lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n = m: Nat
m * n: Nat
n := by
Goals accomplished! 🐙
  m, n: Nat

gcd m n * lcm m n = m * nrw [m, n: Nat

gcd m n * lcm m n = m * nlcm: Nat → Nat → Nat
lcm,m, n: Nat

gcd m n * (m * n / gcd m n) = m * n m, n: Nat

gcd m n * lcm m n = m * nNat.mul_div_cancel': ∀ {n m : Nat}, n ∣ m → n * (m / n) = m
Nat.mul_div_cancel' (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left m: Nat
m n: Nat
n) (Nat.dvd_mul_right: ∀ (a b : Nat), a ∣ a * b
Nat.dvd_mul_right m: Nat
m n: Nat
n))m, n: Nat

m * n = m * n]
Goals accomplished! 🐙

theorem lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd {m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat} (H1: m ∣ k
H1 : m: Nat
m ∣ k: Nat
k) (H2: n ∣ k
H2 : n: Nat
n ∣ k: Nat
k) : lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n ∣ k: Nat
k := by
Goals accomplished! 🐙
  m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

lcm m n ∣ kmatch eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos k: Nat
k with
  m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

lcm m n ∣ k| .inl: ∀ {a b : Prop}, a → a ∨ b
.inl h: k = 0
h =>m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ k m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

lcm m n ∣ krw [m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ kh: k = 0
hm, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ 0]m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ 0;m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ 0 m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0

lcm m n ∣ kexact Nat.dvd_zero: ∀ (a : Nat), a ∣ 0
Nat.dvd_zero _: Nat
_
Goals accomplished! 🐙
  m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

lcm m n ∣ k| .inr: ∀ {a b : Prop}, b → a ∨ b
.inr kpos: k > 0
kpos =>m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

lcm m n ∣ k
    m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

lcm m n ∣ kapply Nat.dvd_of_mul_dvd_mul_left: ∀ {k m n : Nat}, 0 < k → k * m ∣ k * n → m ∣ n
Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
gcd_pos_of_pos_left n: Nat
n (pos_of_dvd_of_pos: ∀ {m n : Nat}, m ∣ n → 0 < n → 0 < m
pos_of_dvd_of_pos H1: m ∣ k
H1 kpos: k > 0
kpos))m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

gcd m n * lcm m n ∣ gcd m n * k
    m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

lcm m n ∣ krw [m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

gcd m n * lcm m n ∣ gcd m n * kgcd_mul_lcm: ∀ (m n : Nat), gcd m n * lcm m n = m * n
gcd_mul_lcm,m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

m * n ∣ gcd m n * k m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

gcd m n * lcm m n ∣ gcd m n * k← gcd_mul_right: ∀ (m n k : Nat), gcd (m * n) (k * n) = gcd m k * n
gcd_mul_right,m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

m * n ∣ gcd (m * k) (n * k) m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

gcd m n * lcm m n ∣ gcd m n * kNat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm n: Nat
n k: Nat
km, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

m * n ∣ gcd (m * k) (k * n)]m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

m * n ∣ gcd (m * k) (k * n)
    m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0

lcm m n ∣ kexact dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.mul_dvd_mul_left: ∀ {b c : Nat} (a : Nat), b ∣ c → a * b ∣ a * c
Nat.mul_dvd_mul_left _: Nat
_ H2: n ∣ k
H2) (Nat.mul_dvd_mul_right: ∀ {a b : Nat}, a ∣ b → ∀ (c : Nat), a * c ∣ b * c
Nat.mul_dvd_mul_right H1: m ∣ k
H1 _: Nat
_)
Goals accomplished! 🐙

theorem lcm_assoc: ∀ (m n k : Nat), lcm (lcm m n) k = lcm m (lcm n k)
lcm_assoc (m: Nat
m n: Nat
n k: Nat
k : Nat: Type
Nat) : lcm: Nat → Nat → Nat
lcm (lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n) k: Nat
k = lcm: Nat → Nat → Nat
lcm m: Nat
m (lcm: Nat → Nat → Nat
lcm n: Nat
n k: Nat
k) :=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
  (lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
    (lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd (dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left m: Nat
m (lcm: Nat → Nat → Nat
lcm n: Nat
n k: Nat
k)) (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left n: Nat
n k: Nat
k) (dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right m: Nat
m (lcm: Nat → Nat → Nat
lcm n: Nat
n k: Nat
k))))
    (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right n: Nat
n k: Nat
k) (dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right m: Nat
m (lcm: Nat → Nat → Nat
lcm n: Nat
n k: Nat
k))))
  (lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
    (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left m: Nat
m n: Nat
n) (dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left (lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n) k: Nat
k))
    (lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd (Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans (dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right m: Nat
m n: Nat
n) (dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left (lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n) k: Nat
k))
      (dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right (lcm: Nat → Nat → Nat
lcm m: Nat
m n: Nat
n) k: Nat
k)))

theorem lcm_ne_zero: ∀ {m n : Nat}, m ≠ 0 → n ≠ 0 → lcm m n ≠ 0
lcm_ne_zero (hm: m ≠ 0
hm : m: ?m.6758
m ≠ 0: ?m.6784
0) (hn: n ≠ 0
hn : n: ?m.6778
n ≠ 0: ?m.6798
0) : lcm: Nat → Nat → Nat
lcm m: ?m.6758
m n: ?m.6778
n ≠ 0: ?m.6812
0 := by
Goals accomplished! 🐙
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

lcm m n ≠ 0intro h: lcm m n = 0
hm, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

False
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

lcm m n ≠ 0have h1: ?m.6835
h1 := gcd_mul_lcm: ∀ (m n : Nat), gcd m n * lcm m n = m * n
gcd_mul_lcm m: Nat
m n: Nat
nm, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n

False
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

lcm m n ≠ 0rw [m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n

Falseh: lcm m n = 0
h,m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * 0 = m * n

False m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n

FalseNat.mul_zero: ∀ (n : Nat), n * 0 = 0
Nat.mul_zerom, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

False]m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

False at h1: gcd m n * 0 = m * n
h1m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

False
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

lcm m n ≠ 0match mul_eq_zero: ∀ {n m : Nat}, n * m = 0 ↔ n = 0 ∨ m = 0
mul_eq_zero.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h1: 0 = m * n
h1.symm: ∀ {α : Sort ?u.6884} {a b : α}, a = b → b = a
symm with
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

False| .inl: ∀ {a b : Prop}, a → a ∨ b
.inl hm1: m = 0
hm1 =>m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

hm1: m = 0

False m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

Falseexact hm: m ≠ 0
hm hm1: m = 0
hm1
Goals accomplished! 🐙
  m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

False| .inr: ∀ {a b : Prop}, b → a ∨ b
.inr hn1: n = 0
hn1 =>m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

hn1: n = 0

False m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

Falseexact hn: n ≠ 0
hn hn1: n = 0
hn1
Goals accomplished! 🐙

/-!
### `coprime`

See also `nat.coprime_of_dvd` and `nat.coprime_of_dvd'` to prove `nat.coprime m n`.
-/

instance: (m n : Nat) → Decidable (coprime m n)
instance (m: Nat
m n: Nat
n : Nat: Type
Nat) : Decidable: Prop → Type
Decidable (coprime: Nat → Nat → Prop
coprime m: Nat
m n: Nat
n) := inferInstanceAs: (α : Sort ?u.7015) → [i : α] → α
inferInstanceAs (Decidable: Prop → Type
Decidable (_: ?m.7018
_ = 1: ?m.7021
1))

theorem coprime_iff_gcd_eq_one: ∀ {m n : Nat}, coprime m n ↔ gcd m n = 1
coprime_iff_gcd_eq_one : coprime: Nat → Nat → Prop
coprime m: ?m.7130
m n: ?m.7134
n ↔ gcd: Nat → Nat → Nat
gcd m: ?m.7130
m n: ?m.7134
n = 1: ?m.7139
1 := .rfl: ∀ {a : Prop}, a ↔ a
.rfl

theorem coprime.gcd_eq_one: ∀ {m n : Nat}, coprime m n → gcd m n = 1
coprime.gcd_eq_one : coprime: Nat → Nat → Prop
coprime m: ?m.7168
m n: ?m.7173
n → gcd: Nat → Nat → Nat
gcd m: ?m.7168
m n: ?m.7173
n = 1: ?m.7180
1 := id: ∀ {α : Sort ?u.7201}, α → α
id

theorem coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm : coprime: Nat → Nat → Prop
coprime n: ?m.7211
n m: ?m.7216
m → coprime: Nat → Nat → Prop
coprime m: ?m.7216
m n: ?m.7211
n := (gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm m: Nat
m n: Nat
n).trans: ∀ {α : Sort ?u.7227} {a b c : α}, a = b → b = c → a = c
trans

theorem coprime_comm: ∀ {n m : Nat}, coprime n m ↔ coprime m n
coprime_comm : coprime: Nat → Nat → Prop
coprime n: ?m.7248
n m: ?m.7252
m ↔ coprime: Nat → Nat → Prop
coprime m: ?m.7252
m n: ?m.7248
n := ⟨coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm, coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm⟩

theorem coprime.dvd_of_dvd_mul_right: ∀ {k n m : Nat}, coprime k n → k ∣ m * n → k ∣ m
coprime.dvd_of_dvd_mul_right (H1: coprime k n
H1 : coprime: Nat → Nat → Prop
coprime k: ?m.7282
k n: ?m.7286
n) (H2: k ∣ m * n
H2 : k: ?m.7282
k ∣ m: ?m.7300
m * n: ?m.7286
n) : k: ?m.7282
k ∣ m: ?m.7300
m := by
Goals accomplished! 🐙
  k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

k ∣ mlet t: ?m.7367
t := dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd (Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left k: Nat
k m: Nat
m) H2: k ∣ m * n
H2k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)

k ∣ m
  k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

k ∣ mrwa [k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)

k ∣ mgcd_mul_left: ∀ (m n k : Nat), gcd (m * n) (m * k) = m * gcd n k
gcd_mul_left,k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t: k ∣ m * gcd k n

k ∣ m k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)

k ∣ mH1: coprime k n
H1.gcd_eq_one: ∀ {m n : Nat}, coprime m n → gcd m n = 1
gcd_eq_one,k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t: k ∣ m * 1

k ∣ m k, n, m: Nat

H1: coprime k n

H2: