[GOAL]
⊢ WellFounded DvdNotUnit
[PROOFSTEP]
refine'
  RelHomClass.wellFounded (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, _⟩ : DvdNotUnit →r (· < ·))
    (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
[GOAL]
⊢ ∀ {a b : ℕ}, DvdNotUnit a b → (fun x => if x = 0 then ⊤ else ↑x) a < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
intro a b h
[GOAL]
a b : ℕ
h : DvdNotUnit a b
⊢ (fun x => if x = 0 then ⊤ else ↑x) a < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
cases' a with a
[GOAL]
case zero
b : ℕ
h : DvdNotUnit zero b
⊢ (fun x => if x = 0 then ⊤ else ↑x) zero < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
b : ℕ
h : DvdNotUnit zero b
⊢ False
[PROOFSTEP]
revert h
[GOAL]
case zero.h
b : ℕ
⊢ DvdNotUnit zero b → False
[PROOFSTEP]
simp [DvdNotUnit]
[GOAL]
case succ
b a : ℕ
h : DvdNotUnit (succ a) b
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) b
[PROOFSTEP]
cases b
[GOAL]
case succ.zero
a : ℕ
h : DvdNotUnit (succ a) zero
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) zero
[PROOFSTEP]
simpa [succ_ne_zero] using WithTop.coe_lt_top (a + 1)
[GOAL]
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) (succ n✝)
[PROOFSTEP]
cases' dvd_and_not_dvd_iff.2 h with h1 h2
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
⊢ (fun x => if x = 0 then ⊤ else ↑x) (succ a) < (fun x => if x = 0 then ⊤ else ↑x) (succ n✝)
[PROOFSTEP]
simp only [succ_ne_zero, cast_lt, if_false]
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
⊢ succ a < succ n✝
[PROOFSTEP]
refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_
[GOAL]
case succ.succ.intro
a n✝ : ℕ
h : DvdNotUnit (succ a) (succ n✝)
h1 : succ a ∣ succ n✝
h2 : ¬succ n✝ ∣ succ a
con : succ a = succ n✝
⊢ succ n✝ ∣ succ a
[PROOFSTEP]
rw [con]
[GOAL]
a b : ℕ
⊢ Associated (Nat.gcd a b * Nat.lcm a b) (a * b)
[PROOFSTEP]
rw [Nat.gcd_mul_lcm]
[GOAL]
a b : ℕ
⊢ Associated (a * b) (a * b)
[PROOFSTEP]
rfl
[GOAL]
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hna.lt_or_lt with ha ha
[GOAL]
case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hnb.lt_or_lt with hb hb
[GOAL]
case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
cases' hnb.lt_or_lt with hb hb
[GOAL]
case inl.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : b < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inl.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
hb : 0 < b
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inr.inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : b < 0
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
case inr.inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ (fun a => if 0 ≤ a then 1 else -1) (a * b) =
    (fun a => if 0 ≤ a then 1 else -1) a * (fun a => if 0 ≤ a then 1 else -1) b
[PROOFSTEP]
simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
[GOAL]
u : ℤˣ
eq : u = -1
⊢ -1 < 0
[PROOFSTEP]
decide
[GOAL]
z : ℤ
h : 0 ≤ z
⊢ ↑normalize z = z
[PROOFSTEP]
rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]
[GOAL]
z : ℤ
h : z ≤ 0
⊢ ↑normalize z = -z
[PROOFSTEP]
obtain rfl | h := h.eq_or_lt
[GOAL]
case inl
h : 0 ≤ 0
⊢ ↑normalize 0 = -0
[PROOFSTEP]
simp
[GOAL]
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ ↑normalize z = -z
[PROOFSTEP]
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one, mul_neg_one]
[GOAL]
z : ℤ
⊢ |z| = ↑normalize z
[PROOFSTEP]
cases le_total 0 z
[GOAL]
case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = ↑normalize z
[PROOFSTEP]
simp [-normalize_apply, normalize_of_nonneg, normalize_of_nonpos, *]
[GOAL]
case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = ↑normalize z
[PROOFSTEP]
simp [-normalize_apply, normalize_of_nonneg, normalize_of_nonpos, *]
[GOAL]
z : ℤ
hz : ↑normalize z = z
⊢ |z| = z
[PROOFSTEP]
rw [abs_eq_normalize, hz]
[GOAL]
a b : ℤ
⊢ Associated ((fun a b => ↑(gcd a b)) a b * (fun a b => ↑(lcm a b)) a b) (a * b)
[PROOFSTEP]
rw [← Int.ofNat_mul, gcd_mul_lcm, coe_natAbs, abs_eq_normalize]
[GOAL]
a b : ℤ
⊢ Associated (↑normalize (a * b)) (a * b)
[PROOFSTEP]
exact normalize_associated (a * b)
[GOAL]
a : ℤ
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
cases' natAbs_eq a with h h
[GOAL]
case inl
a : ℤ
h : a = ↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
use 1, isUnit_one
[GOAL]
case h
a : ℤ
h : a = ↑(natAbs a)
⊢ ↑(natAbs a) = 1 * a
[PROOFSTEP]
rw [← h, one_mul]
[GOAL]
case inr
a : ℤ
h : a = -↑(natAbs a)
⊢ ∃ u x, ↑(natAbs a) = u * a
[PROOFSTEP]
use-1, isUnit_one.neg
[GOAL]
case h
a : ℤ
h : a = -↑(natAbs a)
⊢ ↑(natAbs a) = -1 * a
[PROOFSTEP]
rw [← neg_eq_iff_eq_neg.mpr h]
[GOAL]
case h
a : ℤ
h : a = -↑(natAbs a)
⊢ -a = -1 * a
[PROOFSTEP]
simp only [neg_mul, one_mul]
[GOAL]
a b : ℤ
⊢ gcd a b = 1 ↔ IsCoprime a b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
⊢ gcd a b = 1 → IsCoprime a b
[PROOFSTEP]
intro hg
[GOAL]
case mp
a b : ℤ
hg : gcd a b = 1
⊢ IsCoprime a b
[PROOFSTEP]
obtain ⟨ua, -, ha⟩ := exists_unit_of_abs a
[GOAL]
case mp.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
⊢ IsCoprime a b
[PROOFSTEP]
obtain ⟨ub, -, hb⟩ := exists_unit_of_abs b
[GOAL]
case mp.intro.intro.intro.intro
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ IsCoprime a b
[PROOFSTEP]
use Nat.gcdA (Int.natAbs a) (Int.natAbs b) * ua, Nat.gcdB (Int.natAbs a) (Int.natAbs b) * ub
[GOAL]
case h
a b : ℤ
hg : gcd a b = 1
ua : ℤ
ha : ↑(natAbs a) = ua * a
ub : ℤ
hb : ↑(natAbs b) = ub * b
⊢ Nat.gcdA (natAbs a) (natAbs b) * ua * a + Nat.gcdB (natAbs a) (natAbs b) * ub * b = 1
[PROOFSTEP]
rw [mul_assoc, ← ha, mul_assoc, ← hb, mul_comm, mul_comm _ (Int.natAbs b : ℤ), ← Nat.gcd_eq_gcd_ab, ← gcd_eq_natAbs, hg,
  Int.ofNat_one]
[GOAL]
case mpr
a b : ℤ
⊢ IsCoprime a b → gcd a b = 1
[PROOFSTEP]
rintro ⟨r, s, h⟩
[GOAL]
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
⊢ gcd a b = 1
[PROOFSTEP]
by_contra hg
[GOAL]
case mpr.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
⊢ False
[PROOFSTEP]
obtain ⟨p, ⟨hp, ha, hb⟩⟩ := Nat.Prime.not_coprime_iff_dvd.mp hg
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ False
[PROOFSTEP]
apply Nat.Prime.not_dvd_one hp
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ p ∣ 1
[PROOFSTEP]
rw [← coe_nat_dvd, Int.ofNat_one, ← h]
[GOAL]
case mpr.intro.intro.intro.intro.intro
a b r s : ℤ
h : r * a + s * b = 1
hg : ¬gcd a b = 1
p : ℕ
hp : Nat.Prime p
ha : p ∣ natAbs a
hb : p ∣ natAbs b
⊢ ↑p ∣ r * a + s * b
[PROOFSTEP]
exact dvd_add ((coe_nat_dvd_left.mpr ha).mul_left _) ((coe_nat_dvd_left.mpr hb).mul_left _)
[GOAL]
a b : ℤ
⊢ IsCoprime a b ↔ Nat.coprime (natAbs a) (natAbs b)
[PROOFSTEP]
rw [← gcd_eq_one_iff_coprime, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
[GOAL]
a : ℤ
m n : ℕ
⊢ gcd a (↑m * ↑n) ≠ 1 ↔ gcd a ↑m ≠ 1 ∨ gcd a ↑n ≠ 1
[PROOFSTEP]
simp only [gcd_eq_one_iff_coprime, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
have h' : IsUnit (GCDMonoid.gcd a b) := by
  rw [← coe_gcd, h, Int.ofNat_one]
  exact isUnit_one
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)
[PROOFSTEP]
rw [← coe_gcd, h, Int.ofNat_one]
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq
[GOAL]
case intro.intro
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
[PROOFSTEP]
use d
[GOAL]
case h
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2
[PROOFSTEP]
rw [← hu]
[GOAL]
case h
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
cases' Int.units_eq_one_or u with hu' hu'
[GOAL]
case h.inl
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
rw [hu']
[GOAL]
case h.inl
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑1 = d ^ 2 ∨ d ^ 2 * ↑1 = -d ^ 2
[PROOFSTEP]
simp
[GOAL]
case h.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
[PROOFSTEP]
rw [hu']
[GOAL]
case h.inr
a b c : ℤ
h : gcd a b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2
[PROOFSTEP]
simp
[GOAL]
a b : ℤ
⊢ natAbs (EuclideanDomain.gcd a b) = gcd a b
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case a
a b : ℤ
⊢ natAbs (EuclideanDomain.gcd a b) ∣ gcd a b
[PROOFSTEP]
rw [← Int.coe_nat_dvd]
[GOAL]
case a
a b : ℤ
⊢ gcd a b ∣ natAbs (EuclideanDomain.gcd a b)
[PROOFSTEP]
rw [← Int.coe_nat_dvd]
[GOAL]
case a
a b : ℤ
⊢ ↑(natAbs (EuclideanDomain.gcd a b)) ∣ ↑(gcd a b)
[PROOFSTEP]
rw [Int.natAbs_dvd]
[GOAL]
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(gcd a b)
[PROOFSTEP]
exact Int.dvd_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
[GOAL]
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ ↑(natAbs (EuclideanDomain.gcd a b))
[PROOFSTEP]
rw [Int.dvd_natAbs]
[GOAL]
case a
a b : ℤ
⊢ ↑(gcd a b) ∣ EuclideanDomain.gcd a b
[PROOFSTEP]
exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left _ _) (Int.gcd_dvd_right _ _)
[GOAL]
⊢ Associates ℤ ≃ ℕ
[PROOFSTEP]
refine' ⟨fun z => z.out.natAbs, fun n => Associates.mk n, _, _⟩
[GOAL]
case refine'_1
⊢ Function.LeftInverse (fun n => Associates.mk ↑n) fun z => Int.natAbs (Associates.out z)
[PROOFSTEP]
refine' fun a =>
  Quotient.inductionOn a fun a => Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, _⟩
[GOAL]
case refine'_1
a✝ : Associates ℤ
a : ℤ
⊢ a * ↑(normUnit a) = ↑((fun z => Int.natAbs (Associates.out z)) (Quotient.mk (Associated.setoid ℤ) a))
[PROOFSTEP]
simp [Int.abs_eq_normalize]
[GOAL]
case refine'_2
⊢ Function.RightInverse (fun n => Associates.mk ↑n) fun z => Int.natAbs (Associates.out z)
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
n : ℕ
⊢ (fun z => Int.natAbs (Associates.out z)) ((fun n => Associates.mk ↑n) n) = n
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
n : ℕ
⊢ Int.natAbs (↑n * ↑(normUnit ↑n)) = n
[PROOFSTEP]
rw [← normalize_apply, ← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_ofNat]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
[PROOFSTEP]
rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.coe_nat_dvd_left]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left, Int.coe_nat_dvd_left]
[GOAL]
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
[PROOFSTEP]
exact Int.Prime.dvd_mul hp h
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left, Int.natAbs_pow] at h 
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ natAbs n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
exact hp.dvd_of_dvd_pow h
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n
[PROOFSTEP]
rw [Int.coe_nat_dvd_left]
[GOAL]
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ natAbs n
[PROOFSTEP]
exact Int.Prime.dvd_pow hp h
[GOAL]
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
cases' Int.Prime.dvd_mul hp h with hp2 hpp
[GOAL]
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
apply Or.intro_left
[GOAL]
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2
[PROOFSTEP]
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)
[GOAL]
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p = 2 ∨ p ∣ Int.natAbs m
[PROOFSTEP]
apply Or.intro_right
[GOAL]
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p ∣ Int.natAbs m
[PROOFSTEP]
rw [sq, Int.natAbs_mul] at hpp 
[GOAL]
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs m * Int.natAbs m
⊢ p ∣ Int.natAbs m
[PROOFSTEP]
exact (or_self_iff _).mp ((Nat.Prime.dvd_mul hp).mp hpp)
[GOAL]
n : ℤ
hn : natAbs n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn
[GOAL]
case intro.intro
n : ℤ
hn : natAbs n ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ natAbs n
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.coe_nat_dvd_left.mpr pd⟩
[GOAL]
n : ℕ
⊢ normalizedFactors n = ↑(factors n)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ normalizedFactors zero = ↑(factors zero)
case succ n✝ : ℕ ⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
[PROOFSTEP]
case zero => simp
[GOAL]
⊢ normalizedFactors zero = ↑(factors zero)
[PROOFSTEP]
case zero => simp
[GOAL]
⊢ normalizedFactors zero = ↑(factors zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ normalizedFactors (succ n✝) = ↑(factors (succ n✝))
[PROOFSTEP]
case succ n =>
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
  · rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
    apply normalizedFactors_prod (Nat.succ_ne_zero _)
  · intro x hx
    rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
    exact Nat.prime_of_mem_factors hx
[GOAL]
n : ℕ
⊢ normalizedFactors (succ n) = ↑(factors (succ n))
[PROOFSTEP]
case succ n =>
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
  · rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
    apply normalizedFactors_prod (Nat.succ_ne_zero _)
  · intro x hx
    rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
    exact Nat.prime_of_mem_factors hx
[GOAL]
n : ℕ
⊢ normalizedFactors (succ n) = ↑(factors (succ n))
[PROOFSTEP]
rw [← Multiset.rel_eq, ← associated_eq_eq]
[GOAL]
n : ℕ
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (succ n)) ↑(factors (succ n))
[PROOFSTEP]
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
[GOAL]
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (Multiset.prod ↑(factors (succ n)))
[PROOFSTEP]
rw [Multiset.coe_prod, Nat.prod_factors n.succ_ne_zero]
[GOAL]
n : ℕ
⊢ Associated (Multiset.prod (normalizedFactors (succ n))) (succ n)
[PROOFSTEP]
apply normalizedFactors_prod (Nat.succ_ne_zero _)
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ ↑(factors (succ n)) → Irreducible x
[PROOFSTEP]
intro x hx
[GOAL]
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Irreducible x
[PROOFSTEP]
rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
[GOAL]
n x : ℕ
hx : x ∈ ↑(factors (succ n))
⊢ Prime x
[PROOFSTEP]
exact Nat.prime_of_mem_factors hx
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ normalizedFactors (Multiset.prod s) = s
[PROOFSTEP]
rw [← Multiset.rel_eq, ← associated_eq_eq]
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) (normalizedFactors (Multiset.prod s)) s
[PROOFSTEP]
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h (normalizedFactors_prod _)
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ Multiset.prod s ≠ 0
[PROOFSTEP]
rw [Ne.def, Multiset.prod_eq_zero_iff]
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
⊢ ¬0 ∈ s
[PROOFSTEP]
intro con
[GOAL]
s : Multiset ℕ
h : ∀ (x : ℕ), x ∈ s → Irreducible x
con : 0 ∈ s
⊢ False
[PROOFSTEP]
exact not_irreducible_zero (h 0 con)
[GOAL]
a b : ℤ
⊢ Finite a b ↔ Finite (_root_.Int.natAbs a) (_root_.Int.natAbs b)
[PROOFSTEP]
simp only [finite_def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]
[GOAL]
a b : ℤ
⊢ Finite a b ↔ _root_.Int.natAbs a ≠ 1 ∧ b ≠ 0
[PROOFSTEP]
rw [finite_int_iff_natAbs_finite, finite_nat_iff, pos_iff_ne_zero, Int.natAbs_ne_zero]
[GOAL]
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P n
[PROOFSTEP]
apply UniqueFactorizationMonoid.induction_on_prime
[GOAL]
case h₁
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ P 0
[PROOFSTEP]
exact h₀
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (x : ℕ), IsUnit x → P x
[PROOFSTEP]
intro n h
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P n
[PROOFSTEP]
rw [Nat.isUnit_iff.1 h]
[GOAL]
case h₂
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h✝ : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n✝ n : ℕ
h : IsUnit n
⊢ P 1
[PROOFSTEP]
exact h₁
[GOAL]
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n : ℕ
⊢ ∀ (a p : ℕ), a ≠ 0 → Prime p → P a → P (p * a)
[PROOFSTEP]
intro a p _ hp ha
[GOAL]
case h₃
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)
n a p : ℕ
a✝ : a ≠ 0
hp : Prime p
ha : P a
⊢ P (p * a)
[PROOFSTEP]
exact h p a hp.nat_prime ha
[GOAL]
a b : ℤ
⊢ Associated a b ↔ natAbs a = natAbs b
[PROOFSTEP]
rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs, dvd_dvd_iff_associated]
[GOAL]
a b : ℤ
⊢ Associated (natAbs a) (natAbs b) ↔ natAbs a = natAbs b
[PROOFSTEP]
exact associated_iff_eq
[GOAL]
a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b
[PROOFSTEP]
rw [Int.associated_iff_natAbs]
[GOAL]
a b : ℤ
⊢ natAbs a = natAbs b ↔ a = b ∨ a = -b
[PROOFSTEP]
exact Int.natAbs_eq_natAbs_iff
[GOAL]
a : ℤ
⊢ Ideal.span {↑(natAbs a)} = Ideal.span {a}
[PROOFSTEP]
rw [Ideal.span_singleton_eq_span_singleton]
[GOAL]
a : ℤ
⊢ Associated (↑(natAbs a)) a
[PROOFSTEP]
exact (associated_natAbs _).symm
[GOAL]
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : Associated (d ^ bit1 k) a
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
replace hd := hd.symm
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : Associated a (d ^ bit1 k)
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← neg_pow_bit1] at hd 
[GOAL]
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
d : ℤ
hd : a = d ^ bit1 k ∨ a = (-d) ^ bit1 k
⊢ ∃ d, a = d ^ bit1 k
[PROOFSTEP]
obtain rfl | rfl := hd
[GOAL]
case intro.inl
b c : ℤ
k : ℕ
d : ℤ
hab : IsCoprime (d ^ bit1 k) b
h : d ^ bit1 k * b = c ^ bit1 k
⊢ ∃ d_1, d ^ bit1 k = d_1 ^ bit1 k
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case intro.inr
b c : ℤ
k : ℕ
d : ℤ
hab : IsCoprime ((-d) ^ bit1 k) b
h : (-d) ^ bit1 k * b = c ^ bit1 k
⊢ ∃ d_1, (-d) ^ bit1 k = d_1 ^ bit1 k
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
a b c : ℤ
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ bit1 k
⊢ b * a = ?m.195121 hab h ^ bit1 k
[PROOFSTEP]
rwa [mul_comm] at h 
