[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h : p ∣ a ^ n
⊢ p ∣ a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ a ^ Nat.zero
⊢ p ∣ a
[PROOFSTEP]
rw [pow_zero] at h
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
⊢ p ∣ a
[PROOFSTEP]
have := isUnit_of_dvd_one h
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a
[PROOFSTEP]
have := not_unit hp
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n : ℕ
h✝ : p ∣ a ^ n
h : p ∣ 1
this✝ : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a
[PROOFSTEP]
contradiction
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ Nat.succ n
⊢ p ∣ a
[PROOFSTEP]
rw [pow_succ] at h
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a
[PROOFSTEP]
cases' dvd_or_dvd hp h with dvd_a dvd_pow
[GOAL]
case succ.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a
[PROOFSTEP]
assumption
[GOAL]
case succ.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp✝ hp : Prime p
a : α
n✝ : ℕ
h✝ : p ∣ a ^ n✝
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
[PROOFSTEP]
exact ih dvd_pow
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
h : p = 0
⊢ ↑f p = 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b
[PROOFSTEP]
refine'
  (hp.2.2 (f a) (f b) <| by
        convert map_dvd f h
        simp).imp
    _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f p ∣ ↑f a * ↑f b
[PROOFSTEP]
convert map_dvd f h
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f a * ↑f b = ↑f (a * b)
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f p ∣ ↑f a → p ∣ a
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f a
⊢ p ∣ a
[PROOFSTEP]
convert ← map_dvd g h
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f a
⊢ ↑g (↑f p) = p
[PROOFSTEP]
apply hinv
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f a
⊢ ↑g (↑f a) = a
[PROOFSTEP]
apply hinv
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h : p ∣ a * b
⊢ ↑f p ∣ ↑f b → p ∣ b
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f b
⊢ p ∣ b
[PROOFSTEP]
convert ← map_dvd g h
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f b
⊢ ↑g (↑f p) = p
[PROOFSTEP]
apply hinv
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
hinv : ∀ (a : α), ↑g (↑f a) = a
hp : Prime (↑f p)
a b : α
h✝ : p ∣ a * b
h : ↑f p ∣ ↑f b
⊢ ↑g (↑f b) = b
[PROOFSTEP]
apply hinv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
e : α ≃* β
h : Prime p
a : β
⊢ ↑e (↑(symm e) a) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type u_5
G : Type u_6
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
e : α ≃* β
a : α
⊢ ↑(symm e) (↑e a) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
⊢ a ∣ p * b → p ∣ a ∨ a ∣ b
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b
[PROOFSTEP]
rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b c : α
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b
[PROOFSTEP]
exact Or.inl h
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
[PROOFSTEP]
rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b x : α
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b
[PROOFSTEP]
exact Or.inr (hc.symm ▸ dvd_mul_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ p ^ Nat.zero ∣ b
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ a
h'✝ : p ^ n ∣ a * b
h' : p ^ Nat.zero ∣ a * b
⊢ 1 ∣ b
[PROOFSTEP]
exact one_dvd b
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
h'✝ : p ^ n✝ ∣ a * b
n : ℕ
ih : p ^ n ∣ a * b → p ^ n ∣ b
h' : p ^ Nat.succ n ∣ a * b
⊢ p ^ Nat.succ n ∣ b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
[GOAL]
case succ.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ Nat.succ n ∣ p ^ n * c
[PROOFSTEP]
rw [pow_succ']
[GOAL]
case succ.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ^ n * p ∣ p ^ n * c
[PROOFSTEP]
apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
n✝ : ℕ
h : ¬p ∣ a
n : ℕ
c : α
h'✝ : p ^ n✝ ∣ a * (p ^ n * c)
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ Nat.succ n ∣ a * (p ^ n * c)
⊢ p ∣ a * c
[PROOFSTEP]
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ', mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a
[PROOFSTEP]
rw [mul_comm] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a
[PROOFSTEP]
exact hp.pow_dvd_of_dvd_mul_left n h h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
⊢ p ∣ a
[PROOFSTEP]
cases' hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H hbdiv
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ Nat.succ n
⊢ p ∣ a
[PROOFSTEP]
exact hp.dvd_of_dvd_pow H
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a b : α
n : ℕ
hp : Prime p
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hpow : p ^ Nat.succ n ∣ a ^ Nat.succ n * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a
[PROOFSTEP]
obtain ⟨y, hy⟩ := hpow
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ∣ a
[PROOFSTEP]
have : a ^ n.succ * x ^ n = p * y :=
  by
  refine' mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) _
  rw [← mul_assoc _ p, ← pow_succ', ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n), mul_assoc]
    -- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ a ^ Nat.succ n * x ^ n = p * y
[PROOFSTEP]
refine' mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
⊢ p ^ n * (a ^ Nat.succ n * x ^ n) = p ^ n * (p * y)
[PROOFSTEP]
rw [← mul_assoc _ p, ← pow_succ', ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n), mul_assoc]
  -- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
⊢ p ∣ a
[PROOFSTEP]
refine' hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb _)
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
x : α
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : α
hy : a ^ Nat.succ n * (p * x) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x
[PROOFSTEP]
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)
[PROOFSTEP]
rw [pow_two, ← mul_assoc]
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p a : α
n : ℕ
hp : Prime p
y z : α
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ Nat.succ n * (p * (p * z)) ^ n = p ^ Nat.succ n * y
this : a ^ Nat.succ n * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ p ^ (i + 1) ∣ x ∨ p ∣ y
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x
[PROOFSTEP]
intro hy
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
hy : ¬p ∣ y
⊢ p ^ (i + 1) ∣ x
[PROOFSTEP]
induction' i with i ih generalizing x
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ^ (Nat.zero + 1) ∣ x * y
⊢ p ^ (Nat.zero + 1) ∣ x
[PROOFSTEP]
rw [pow_one] at hxy ⊢
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i : ℕ
hxy✝ : p ^ (i + 1) ∣ x✝ * y
hy : ¬p ∣ y
x : α
hxy : p ∣ x * y
⊢ p ∣ x
[PROOFSTEP]
exact (h.dvd_or_dvd hxy).resolve_right hy
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p ^ (Nat.succ i + 1) ∣ x * y
⊢ p ^ (Nat.succ i + 1) ∣ x
[PROOFSTEP]
rw [pow_succ] at hxy ⊢
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x✝ y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x✝ * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x : α
hxy : p * p ^ (i + 1) ∣ x * y
⊢ p * p ^ (i + 1) ∣ x
[PROOFSTEP]
obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy
[GOAL]
case succ.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * x' * y
⊢ p * p ^ (i + 1) ∣ p * x'
[PROOFSTEP]
rw [mul_assoc] at hxy
[GOAL]
case succ.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : CancelCommMonoidWithZero α
p x y : α
h : Prime p
i✝ : ℕ
hxy✝ : p ^ (i✝ + 1) ∣ x * y
hy : ¬p ∣ y
i : ℕ
ih : ∀ {x : α}, p ^ (i + 1) ∣ x * y → p ^ (i + 1) ∣ x
x' : α
hxy : p * p ^ (i + 1) ∣ p * (x' * y)
⊢ p * p ^ (i + 1) ∣ p * x'
[PROOFSTEP]
exact mul_dvd_mul_left p (ih ((mul_dvd_mul_iff_left h.ne_zero).mp hxy))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
⊢ ¬Irreducible 1
[PROOFSTEP]
simp [irreducible_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
n : ℕ
hn : n ≠ 1
⊢ Irreducible (x ^ n) → IsUnit x
[PROOFSTEP]
obtain hn | hn := hn.lt_or_lt
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : n < 1
⊢ Irreducible (x ^ n) → IsUnit x
[PROOFSTEP]
simp only [Nat.lt_one_iff.mp hn, IsEmpty.forall_iff, not_irreducible_one, pow_zero]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
⊢ Irreducible (x ^ n) → IsUnit x
[PROOFSTEP]
intro h
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
h : Irreducible (x ^ n)
⊢ IsUnit x
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hn
[GOAL]
case inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x ^ (1 + k + 1))
⊢ IsUnit x
[PROOFSTEP]
rw [pow_succ, add_comm] at h
[GOAL]
case inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x * x ^ (k + 1))
⊢ IsUnit x
[PROOFSTEP]
exact (or_iff_left_of_imp isUnit_pow_succ_iff.mp).mp (of_irreducible_mul h)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h : ¬IsUnit x
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
[PROOFSTEP]
haveI := Classical.dec
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
[PROOFSTEP]
refine' or_iff_not_imp_right.2 fun H => _
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x
[PROOFSTEP]
simp [h, irreducible_iff] at H ⊢
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : α), x = a * b → IsUnit a ∨ IsUnit b
[PROOFSTEP]
refine' fun a b h => by_contradiction fun o => _
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False
[PROOFSTEP]
simp [not_or] at o
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
α : Type u_5
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False
[PROOFSTEP]
exact H _ o.1 _ o.2 h.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p q : α
hp : Irreducible p
hq : Irreducible q
⊢ p ∣ q → q ∣ p
[PROOFSTEP]
rintro ⟨q', rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p : α
hp : Irreducible p
q' : α
hq : Irreducible (p * q')
⊢ p * q' ∣ p
[PROOFSTEP]
rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_unit)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
⊢ Irreducible (↑a * b) ↔ Irreducible b
[PROOFSTEP]
simp only [irreducible_iff, Units.isUnit_units_mul, and_congr_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : α), ↑a * b = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
[PROOFSTEP]
refine' fun _ => ⟨fun h A B HAB => _, fun h A B HAB => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B
[PROOFSTEP]
rw [← a.isUnit_units_mul]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit (↑a * A) ∨ IsUnit B
[PROOFSTEP]
apply h
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ ↑a * b = ↑a * A * B
[PROOFSTEP]
rw [mul_assoc, ← HAB]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit A ∨ IsUnit B
[PROOFSTEP]
rw [← a⁻¹.isUnit_units_mul]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit (↑a⁻¹ * A) ∨ IsUnit B
[PROOFSTEP]
apply h
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ b = ↑a⁻¹ * A * B
[PROOFSTEP]
rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
⊢ Irreducible (b * ↑a) ↔ Irreducible b
[PROOFSTEP]
simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : α), b * ↑a = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
[PROOFSTEP]
refine' fun _ => ⟨fun h A B HAB => _, fun h A B HAB => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B
[PROOFSTEP]
rw [← Units.isUnit_mul_units B a]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a)
[PROOFSTEP]
apply h
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ b * ↑a = A * (B * ↑a)
[PROOFSTEP]
rw [← mul_assoc, ← HAB]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit B
[PROOFSTEP]
rw [← Units.isUnit_mul_units B a⁻¹]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a⁻¹)
[PROOFSTEP]
apply h
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : b * ↑a = A * B
⊢ b = A * (B * ↑a⁻¹)
[PROOFSTEP]
rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
⊢ Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
⊢ Irreducible (a * b) → Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a
[PROOFSTEP]
refine' fun h => Or.imp (fun h' => ⟨_, h'⟩) (fun h' => ⟨_, h'⟩) (h.isUnit_or_isUnit rfl).symm
[GOAL]
case mp.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit b
⊢ Irreducible a
[PROOFSTEP]
rwa [irreducible_mul_isUnit h'] at h
[GOAL]
case mp.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit a
⊢ Irreducible b
[PROOFSTEP]
rwa [irreducible_isUnit_mul h'] at h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
⊢ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a → Irreducible (a * b)
[PROOFSTEP]
rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
[GOAL]
case mpr.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
ha : Irreducible a
hb : IsUnit b
⊢ Irreducible (a * b)
[PROOFSTEP]
rwa [irreducible_mul_isUnit hb]
[GOAL]
case mpr.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
hb : Irreducible b
ha : IsUnit a
⊢ Irreducible (a * b)
[PROOFSTEP]
rwa [irreducible_isUnit_mul ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : α
ha : Irreducible a
⊢ ¬IsSquare a
[PROOFSTEP]
rintro ⟨b, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
b : α
ha : Irreducible (b * b)
⊢ False
[PROOFSTEP]
simp only [irreducible_mul_iff, or_self_iff] at ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
b : α
ha : Irreducible b ∧ IsUnit b
⊢ False
[PROOFSTEP]
exact ha.1.not_unit ha.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
h : a = 0
⊢ False
[PROOFSTEP]
simp [Prime] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
h : a = 0
⊢ False
[PROOFSTEP]
rw [h, zero_mul] at hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = 0
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
h : a = 0
⊢ False
[PROOFSTEP]
have := hp.left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = 0
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
h : a = 0
this : ¬p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
⊢ 1 * a = b * x * a
[PROOFSTEP]
conv =>
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
| 1 * a = b * x * a
[PROOFSTEP]
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
| 1 * a = b * x * a
[PROOFSTEP]
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
| 1 * a = b * x * a
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
| 1 * a
[PROOFSTEP]
rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ a
x : α
hx : a = a * b * x
⊢ 1 * (a * b * x) = b * x * a
[PROOFSTEP]
simp [mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
h : b = 0
⊢ False
[PROOFSTEP]
simp [Prime] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
h : b = 0
⊢ False
[PROOFSTEP]
rw [h, mul_zero] at hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = 0
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
h : b = 0
⊢ False
[PROOFSTEP]
have := hp.left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : ¬p = 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
a b : α
hab : p = 0
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
h : b = 0
this : ¬p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
⊢ 1 * b = a * x * b
[PROOFSTEP]
conv =>
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
| 1 * b = a * x * b
[PROOFSTEP]
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
| 1 * b = a * x * b
[PROOFSTEP]
  lhs
  rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
| 1 * b = a * x * b
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
| 1 * b
[PROOFSTEP]
rw [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
hab : p = a * b
x✝ : a * b ∣ b
x : α
hx : b = a * b * x
⊢ 1 * (a * b * x) = a * x * b
[PROOFSTEP]
simp [mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
[PROOFSTEP]
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z
[PROOFSTEP]
rwa [mul_right_inj' hp0] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ x
d : α
hd : x = p * d
⊢ a = p ^ (k + 1) * d
[PROOFSTEP]
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ y
d : α
hd : y = p * d
⊢ b = p ^ (l + 1) * d
[PROOFSTEP]
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
x : α
⊢ x * ↑1 = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
x : α
u : αˣ
⊢ x * ↑u * ↑u⁻¹ = x
[PROOFSTEP]
rw [mul_assoc, Units.mul_inv, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
x : α
u v : αˣ
⊢ x * ↑(u * v) = x * ↑u * ↑v
[PROOFSTEP]
rw [Units.val_mul, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a : α
x✝ : IsUnit a
c : αˣ
h : ↑c = a
⊢ 1 * ↑c = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a : α
h : a ~ᵤ 0
⊢ a = 0
[PROOFSTEP]
let ⟨u, h⟩ := h.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a : α
h✝ : a ~ᵤ 0
u : αˣ
h : 0 * ↑u = a
⊢ a = 0
[PROOFSTEP]
simpa using h.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
u : αˣ
h : a * b * ↑u = 1
⊢ a * (b * ↑u) = 1
[PROOFSTEP]
simpa [mul_assoc] using h
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
β : Type u_5
inst✝ : CommMonoid β
a u : β
hu : IsUnit u
⊢ u * a ~ᵤ a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
β : Type u_5
inst✝ : CommMonoid β
a u : β
hu : IsUnit u
⊢ a * u ~ᵤ a
[PROOFSTEP]
exact associated_mul_unit_left _ _ hu
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
β : Type u_5
inst✝ : CommMonoid β
u a b : β
hu : IsUnit u
⊢ u * a ~ᵤ b ↔ a ~ᵤ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
β : Type u_5
inst✝ : CommMonoid β
u a b : β
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
[PROOFSTEP]
exact associated_mul_isUnit_left_iff hu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a₁ a₂ b₁ b₂ : α
c₁ : αˣ
h₁ : a₁ * ↑c₁ = b₁
c₂ : αˣ
h₂ : a₂ * ↑c₂ = b₂
⊢ a₁ * a₂ * ↑(c₁ * c₂) = b₁ * b₂
[PROOFSTEP]
simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
n : ℕ
h : a ~ᵤ b
⊢ a ^ n ~ᵤ b ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ a ^ Nat.zero ~ᵤ b ^ Nat.zero
[PROOFSTEP]
simp [h]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
⊢ 1 ~ᵤ 1
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ Nat.succ n ~ᵤ b ^ Nat.succ n
[PROOFSTEP]
convert h.mul_mul ih
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ Nat.succ n = a * a ^ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ b ^ Nat.succ n = b * b ^ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ a ~ᵤ b
[PROOFSTEP]
rcases hab with ⟨c, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c : α
hba : a * c ∣ a
⊢ a ~ᵤ a * c
[PROOFSTEP]
rcases hba with ⟨d, a_eq⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
⊢ a ~ᵤ a * c
[PROOFSTEP]
by_cases ha0 : a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c
[PROOFSTEP]
simp_all
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
ha0 : a = 0
⊢ 0 ~ᵤ 0
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c
[PROOFSTEP]
have hac0 : a * c ≠ 0 := by
  intro con
  rw [con, zero_mul] at a_eq
  apply ha0 a_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a * c ≠ 0
[PROOFSTEP]
intro con
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
⊢ False
[PROOFSTEP]
rw [con, zero_mul] at a_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False
[PROOFSTEP]
apply ha0 a_eq
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c
[PROOFSTEP]
have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a * (c * d) = a * 1
[PROOFSTEP]
rw [← mul_assoc, ← a_eq, mul_one]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
⊢ a ~ᵤ a * c
[PROOFSTEP]
have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a ~ᵤ a * c
[PROOFSTEP]
have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c * (d * c) = a * c * 1
[PROOFSTEP]
rw [← mul_assoc, ← a_eq, mul_one]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
⊢ a ~ᵤ a * c
[PROOFSTEP]
have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
hdc : d * c = 1
⊢ a ~ᵤ a * c
[PROOFSTEP]
exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0
[PROOFSTEP]
let ⟨u, hu⟩ := h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
ha : a = 0
u : αˣ
hu : a * ↑u = b
⊢ b = 0
[PROOFSTEP]
simp [hu.symm, ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
hb : b = 0
⊢ a = 0
[PROOFSTEP]
let ⟨u, hu⟩ := h.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
hb : b = 0
u : αˣ
hu : b * ↑u = a
⊢ a = 0
[PROOFSTEP]
simp [hu.symm, hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
x✝ : IsUnit q
v : αˣ
hv : ↑v = q
⊢ ↑(v * u⁻¹) = p
[PROOFSTEP]
simp [hv, hu.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
⊢ ∀ (a b : α), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b
[PROOFSTEP]
simp [Units.mul_right_dvd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
⊢ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
intro a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
a b : α
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
exact hp.dvd_or_dvd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
a b : α
h : a ~ᵤ b
u : αˣ
hu : a * ↑u = b
x✝ : IsUnit a
v : αˣ
hv : ↑v = a
⊢ ↑(v * u) = b
[PROOFSTEP]
simp [hv, hu.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ p = p * ↑u * ↑u⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ p * ↑u * ↑u⁻¹ = a * (b * ↑u⁻¹)
[PROOFSTEP]
rw [hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
[PROOFSTEP]
simp [hab, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
hpab : p = a * (b * ↑u⁻¹)
x✝ : IsUnit (b * ↑u⁻¹)
v : αˣ
hv : ↑v = b * ↑u⁻¹
⊢ ↑(v * u) = b
[PROOFSTEP]
simp [hv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a b c d : α
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : αˣ
hu : a * b * ↑u = c * d
v : αˣ
hv : c * ↑v = a
⊢ a * (b * ↑(u * v)) = a * d
[PROOFSTEP]
rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a b c d : α
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : αˣ
hu : a * b * ↑u = c * d
v : αˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
[PROOFSTEP]
simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a b c d : α
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
[PROOFSTEP]
rw [mul_comm a, mul_comm c]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a b c d : α
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
[PROOFSTEP]
exact Associated.of_mul_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p₁ p₂ : α
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
[PROOFSTEP]
have : p₁ ∣ p₂ ^ k₂ := by
  rw [← h.dvd_iff_dvd_right]
  apply dvd_pow_self _ hk₁.ne'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p₁ p₂ : α
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₂ ^ k₂
[PROOFSTEP]
rw [← h.dvd_iff_dvd_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p₁ p₂ : α
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₁ ^ k₁
[PROOFSTEP]
apply dvd_pow_self _ hk₁.ne'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p₁ p₂ : α
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
[PROOFSTEP]
rw [← hp₁.dvd_prime_iff_associated hp₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p₁ p₂ : α
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂
[PROOFSTEP]
exact hp₁.dvd_of_dvd_pow this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x ~ᵤ y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x ~ᵤ y → x = y
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
c : αˣ
⊢ x = x * ↑c
[PROOFSTEP]
rw [units_eq_one c, Units.val_one, mul_one]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x y : α
⊢ x = y → x ~ᵤ y
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x : α
⊢ x ~ᵤ x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
⊢ Associated = Eq
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x✝¹ x✝ : α
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝
[PROOFSTEP]
rw [associated_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : Monoid α
inst✝² : Unique αˣ
M : Type u_5
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q
[PROOFSTEP]
rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : Type u_5
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂
[PROOFSTEP]
rw [← associated_iff_eq] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : Type u_5
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h✝ : p₁ ^ k₁ = p₂ ^ k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
[PROOFSTEP]
apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : Type u_5
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂
[PROOFSTEP]
rw [← associated_iff_eq] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : Type u_5
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h✝ : p₁ ^ k₁ = p₂ ^ k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
[PROOFSTEP]
apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Subsingleton α
a : Associates α
⊢ a = default
[PROOFSTEP]
apply Quotient.recOnSubsingleton₂
[GOAL]
case g
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Subsingleton α
a : Associates α
⊢ ∀ (a b : α), Quotient.mk (Associated.setoid α) a = Quotient.mk (Associated.setoid α) b
[PROOFSTEP]
intro a b
[GOAL]
case g
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Subsingleton α
a✝ : Associates α
a b : α
⊢ Quotient.mk (Associated.setoid α) a = Quotient.mk (Associated.setoid α) b
[PROOFSTEP]
congr
[GOAL]
case g.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Monoid α
inst✝ : Subsingleton α
a✝ : Associates α
a b : α
⊢ a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' b' : Associates α
a₁ a₂ b₁ b₂ : α
x✝¹ : a₁ ≈ b₁
x✝ : a₂ ≈ b₂
c₁ : αˣ
h₁ : a₁ * ↑c₁ = b₁
c₂ : αˣ
h₂ : a₂ * ↑c₂ = b₂
⊢ a₁ * a₂ * ↑(c₁ * c₂) = b₁ * b₂
[PROOFSTEP]
rw [← h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' b' : Associates α
a₁ a₂ b₁ b₂ : α
x✝¹ : a₁ ≈ b₁
x✝ : a₂ ≈ b₂
c₁ : αˣ
h₁ : a₁ * ↑c₁ = b₁
c₂ : αˣ
h₂ : a₂ * ↑c₂ = b₂
⊢ a₁ * a₂ * ↑(c₁ * c₂) = a₁ * ↑c₁ * (a₂ * ↑c₂)
[PROOFSTEP]
simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' b' c' : Associates α
a b c : α
⊢ Quotient.mk (Associated.setoid α) (a * b * c) = Quotient.mk (Associated.setoid α) (a * (b * c))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' : Associates α
a : α
⊢ Quotient.mk (Associated.setoid α) (1 * a) = Quotient.mk (Associated.setoid α) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' : Associates α
a : α
⊢ Quotient.mk (Associated.setoid α) (a * 1) = Quotient.mk (Associated.setoid α) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a' b' : Associates α
a b : α
⊢ Quotient.mk (Associated.setoid α) (a * b) = Quotient.mk (Associated.setoid α) (b * a)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : α
n : ℕ
⊢ Associates.mk (a ^ n) = Associates.mk a ^ n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : α
⊢ Associates.mk (a ^ Nat.zero) = Associates.mk a ^ Nat.zero
[PROOFSTEP]
simp [*, pow_succ, Associates.mk_mul_mk.symm]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : α
n✝ : ℕ
n_ih✝ : Associates.mk (a ^ n✝) = Associates.mk a ^ n✝
⊢ Associates.mk (a ^ Nat.succ n✝) = Associates.mk a ^ Nat.succ n✝
[PROOFSTEP]
simp [*, pow_succ, Associates.mk_mul_mk.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
x y : Associates α
a b : α
h : Quotient.mk (Associated.setoid α) a * Quotient.mk (Associated.setoid α) b = 1
this : a * b ~ᵤ 1
⊢ b * ?m.284131 a b h this ~ᵤ 1
[PROOFSTEP]
rwa [mul_comm] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
x y : Associates α
⊢ x = 1 ∧ y = 1 → x * y = 1
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
u : (Associates α)ˣ
⊢ ↑u = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : Associates α
⊢ IsUnit a ↔ a = ⊥
[PROOFSTEP]
rw [Associates.isUnit_iff_eq_one, bot_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a : α
⊢ IsUnit (Associates.mk a) ↔ a ~ᵤ 1
[PROOFSTEP]
rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b c d : Associates α
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates α
hx : b = a * x
y : Associates α
hy : d = c * y
⊢ b * d = a * c * (x * y)
[PROOFSTEP]
simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : Associates α
⊢ a ≤ b * a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : Associates α
⊢ a ≤ a * b
[PROOFSTEP]
exact le_mul_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
⊢ ∀ (c : α), Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c → a ∣ b
[PROOFSTEP]
intro c hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
⊢ a ∣ b
[PROOFSTEP]
let ⟨d, hd⟩ := (Quotient.exact hc).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
d : αˣ
hd : a * c * ↑d = b
⊢ a ∣ b
[PROOFSTEP]
exact
  ⟨↑d * c,
    calc
      b = a * c * ↑d := hd.symm
      _ = a * (↑d * c) := by ac_rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
d : αˣ
hd : a * c * ↑d = b
⊢ a * c * ↑d = a * (↑d * c)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
x✝ : a ∣ b
c : α
hc : b = a * c
⊢ Associates.mk b = Associates.mk a * Associates.mk c
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
a b : α
x✝ : a ∣ b
c : α
hc : b = a * c
⊢ Associates.mk (a * c) = Associates.mk a * Associates.mk c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
⊢ ∀ (a : Associates α), 0 * a = 0
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a✝ : Associates α
a : α
⊢ 0 * Quot.mk Setoid.r a = 0
[PROOFSTEP]
show Associates.mk (0 * a) = Associates.mk 0
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a✝ : Associates α
a : α
⊢ Associates.mk (0 * a) = Associates.mk 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
⊢ ∀ (a : Associates α), a * 0 = 0
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a✝ : Associates α
a : α
⊢ Quot.mk Setoid.r a * 0 = 0
[PROOFSTEP]
show Associates.mk (a * 0) = Associates.mk 0
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a✝ : Associates α
a : α
⊢ Associates.mk (a * 0) = Associates.mk 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ Prime (Associates.mk p) ↔ Prime p
[PROOFSTEP]
rw [Prime, _root_.Prime, forall_associated]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
trans
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?m.311388
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ Associates.mk p ≠ 0 ↔ ?c
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d
case c
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
case d α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ Prop
[PROOFSTEP]
rfl
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d
case d α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ Prop
[PROOFSTEP]
apply and_congr
[GOAL]
case h₂.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ?h₂.c
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d
case h₂.c
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
case h₂.d α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ Prop
[PROOFSTEP]
rfl
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d
case h₂.d α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ Prop
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h₂.h₂.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ ∀ (a : α),
    (∀ (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
      ?h₂.h₂.q a
case h₂.h₂.q α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ α → Prop
[PROOFSTEP]
intro a
[GOAL]
case h₂.h₂.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p a : α
⊢ (∀ (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.h₂.q a
case h₂.h₂.q α : Type u_1 β : Type u_2 γ : Type u_3 δ : Type u_4 inst✝ : CommMonoidWithZero α p : α ⊢ α → Prop
[PROOFSTEP]
exact forall_associated
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a a_1 : α),
          Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
            Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
apply and_congr mk_ne_zero
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a a_1 : α),
        Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
          Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ¬IsUnit p
[PROOFSTEP]
rw [isUnit_mk]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a a_1 : α),
      Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
        Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
refine' forall₂_congr fun a b => _
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p a b : α
⊢ Associates.mk p ∣ Associates.mk a * Associates.mk b →
      Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk b ↔
    p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
rw [mk_mul_mk, mk_dvd_mk, mk_dvd_mk, mk_dvd_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
⊢ Irreducible (Associates.mk a) ↔ Irreducible a
[PROOFSTEP]
simp only [irreducible_iff, isUnit_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
⊢ (¬IsUnit a ∧ ∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ¬IsUnit a ∧ ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
[PROOFSTEP]
apply and_congr Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : α), a = a_2 * b → IsUnit a_2 ∨ IsUnit b
[PROOFSTEP]
rintro h x y rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
x y : α
h : ∀ (a b : Associates α), Associates.mk (x * y) = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y
[PROOFSTEP]
simpa [isUnit_mk] using h (Associates.mk x) (Associates.mk y) rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : Associates α), Associates.mk a = a_2 * b → IsUnit a_2 ∨ IsUnit b
[PROOFSTEP]
intro h x y
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x y : Associates α
⊢ Associates.mk a = x * y → IsUnit x ∨ IsUnit y
[PROOFSTEP]
refine' Quotient.inductionOn₂ x y fun x y a_eq => _
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
[PROOFSTEP]
rcases Quotient.exact a_eq.symm with ⟨u, a_eq⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * y * ↑u = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
[PROOFSTEP]
rw [mul_assoc] at a_eq
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
[PROOFSTEP]
show IsUnit (Associates.mk x) ∨ IsUnit (Associates.mk y)
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Associates.mk x) ∨ IsUnit (Associates.mk y)
[PROOFSTEP]
simpa [isUnit_mk] using h _ _ a_eq.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
⊢ DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
[PROOFSTEP]
rw [DvdNotUnit, DvdNotUnit, mk_ne_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
apply and_congr_right
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
⊢ a ≠ 0 → ((∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x)
[PROOFSTEP]
intro
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) → ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
contrapose!
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) → ∀ (x : Associates α), ¬IsUnit x → Associates.mk b ≠ Associates.mk a * x
[PROOFSTEP]
rw [forall_associated]
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) →
    ∀ (a_2 : α), ¬IsUnit (Associates.mk a_2) → Associates.mk b ≠ Associates.mk a * Associates.mk a_2
[PROOFSTEP]
intro h x hx hbax
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : Associates.mk b = Associates.mk a * Associates.mk x
⊢ False
[PROOFSTEP]
rw [mk_mul_mk, mk_eq_mk_iff_associated] at hbax
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : b ~ᵤ a * x
⊢ False
[PROOFSTEP]
cases' hbax with u hu
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ False
[PROOFSTEP]
apply h (x * ↑u⁻¹)
[GOAL]
case h.mp.intro._
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)
[PROOFSTEP]
rw [isUnit_mk] at hx
[GOAL]
case h.mp.intro._
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)
[PROOFSTEP]
rw [Associated.isUnit_iff]
[GOAL]
case h.mp.intro._
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit ?m.316875
case h.mp.intro._
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ ?m.316875
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ α
[PROOFSTEP]
apply hx
[GOAL]
case h.mp.intro._
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ x
[PROOFSTEP]
use u
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ * ↑u = x
[PROOFSTEP]
simp
[GOAL]
case h.mp.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ b = a * (x * ↑u⁻¹)
[PROOFSTEP]
simp [← mul_assoc, ← hu]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x
[PROOFSTEP]
rintro ⟨x, ⟨hx, rfl⟩⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ∃ x_1, ¬IsUnit x_1 ∧ Associates.mk (a * x) = Associates.mk a * x_1
[PROOFSTEP]
use Associates.mk x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (Associates.mk x) ∧ Associates.mk (a * x) = Associates.mk a * Associates.mk x
[PROOFSTEP]
simp [isUnit_mk, mk_mul_mk, hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : Associates α
hlt : a < b
⊢ DvdNotUnit a b
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : Associates α
hlt : a < b
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
b : Associates α
hlt : 0 < b
⊢ False
[PROOFSTEP]
apply not_lt_of_le _ hlt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
b : Associates α
hlt : 0 < b
⊢ b ≤ 0
[PROOFSTEP]
apply dvd_zero
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a b : Associates α
hlt : a < b
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : Associates α
x : Associates α
ndvd : ¬a * x ∣ a
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x = a * x_1
[PROOFSTEP]
refine' ⟨x, _, rfl⟩
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : Associates α
x : Associates α
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x
[PROOFSTEP]
contrapose! ndvd
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : Associates α
x : Associates α
ndvd : IsUnit x
⊢ a * x ∣ a
[PROOFSTEP]
rcases ndvd with ⟨u, rfl⟩
[GOAL]
case right.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
a : Associates α
u : (Associates α)ˣ
⊢ a * ↑u ∣ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
⊢ (∀ (a : α), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates α), Irreducible a ↔ Prime a
[PROOFSTEP]
simp_rw [forall_associated, irreducible_mk, prime_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
⊢ CommMonoidWithZero (Associates α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
src✝ : CommMonoidWithZero (Associates α) := inferInstance
⊢ ∀ {a b c : Associates α}, a ≠ 0 → a * b = a * c → b = c
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
[GOAL]
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
src✝ : CommMonoidWithZero (Associates α) := inferInstance
a✝ : Associates α
a : α
b✝ : Associates α
b : α
c✝ : Associates α
c : α
ha : Quot.mk Setoid.r a ≠ 0
h : Quot.mk Setoid.r a * Quot.mk Setoid.r b = Quot.mk Setoid.r a * Quot.mk Setoid.r c
⊢ Quot.mk Setoid.r b = Quot.mk Setoid.r c
[PROOFSTEP]
rcases Quotient.exact' h with ⟨u, hu⟩
[GOAL]
case mk.mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
src✝ : CommMonoidWithZero (Associates α) := inferInstance
a✝ : Associates α
a : α
b✝ : Associates α
b : α
c✝ : Associates α
c : α
ha : Quot.mk Setoid.r a ≠ 0
h : Quot.mk Setoid.r a * Quot.mk Setoid.r b = Quot.mk Setoid.r a * Quot.mk Setoid.r c
u : αˣ
hu : a * b * ↑u = a * c
⊢ Quot.mk Setoid.r b = Quot.mk Setoid.r c
[PROOFSTEP]
have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
src✝ : CommMonoidWithZero (Associates α) := inferInstance
a✝ : Associates α
a : α
b✝ : Associates α
b : α
c✝ : Associates α
c : α
ha : Quot.mk Setoid.r a ≠ 0
h : Quot.mk Setoid.r a * Quot.mk Setoid.r b = Quot.mk Setoid.r a * Quot.mk Setoid.r c
u : αˣ
hu : a * b * ↑u = a * c
⊢ a * (b * ↑u) = a * c
[PROOFSTEP]
rwa [← mul_assoc]
[GOAL]
case mk.mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
src✝ : CommMonoidWithZero (Associates α) := inferInstance
a✝ : Associates α
a : α
b✝ : Associates α
b : α
c✝ : Associates α
c : α
ha : Quot.mk Setoid.r a ≠ 0
h : Quot.mk Setoid.r a * Quot.mk Setoid.r b = Quot.mk Setoid.r a * Quot.mk Setoid.r c
u : αˣ
hu✝ : a * b * ↑u = a * c
hu : a * (b * ↑u) = a * c
⊢ Quot.mk Setoid.r b = Quot.mk Setoid.r c
[PROOFSTEP]
exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
⊢ NoZeroDivisors (Associates α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
a b c : Associates α
ha : a ≠ 0
d : Associates α
hd : a * c = a * b * d
⊢ a * c = a * (b * d)
[PROOFSTEP]
rwa [← mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
⊢ m = 1 ∨ m = p
[PROOFSTEP]
have dvd_rfl' : p ∣ m * d := by rw [r]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
⊢ p ∣ m * d
[PROOFSTEP]
rw [r]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = p
[PROOFSTEP]
rw [r]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
match h m d dvd_rfl' with
| Or.inl h' =>
  by_cases h : m = 0
  case pos => simp [h, zero_mul]
  case neg =>
    rw [r] at h'
    have : m * d ≤ m * 1 := by simpa using h'
    have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
    have : d = 1 := bot_unique this
    simp [this]
| Or.inr h' =>
  by_cases h : d = 0
  case pos =>
    rw [r] at hp0
    have : m * d = 0 := by rw [h]; simp
    contradiction
  case neg =>
    rw [r] at h'
    have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
    exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
by_cases h : m = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case pos => simp [h, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case pos => simp [h, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
simp [h, zero_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case neg =>
  rw [r] at h'
  have : m * d ≤ m * 1 := by simpa using h'
  have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
  have : d = 1 := bot_unique this
  simp [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case neg =>
  rw [r] at h'
  have : m * d ≤ m * 1 := by simpa using h'
  have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
  have : d = 1 := bot_unique this
  simp [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
rw [r] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
have : m * d ≤ m * 1 := by simpa using h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
⊢ m * d ≤ m * 1
[PROOFSTEP]
simpa using h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this : m * d ≤ m * 1
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
have : d ≤ 1 := Associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝ : m * d ≤ m * 1
this : d ≤ 1
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
have : d = 1 := bot_unique this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ m
h : ¬m = 0
this✝¹ : m * d ≤ m * 1
this✝ : d ≤ 1
this : d = 1
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
by_cases h : d = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case pos =>
  rw [r] at hp0
  have : m * d = 0 := by rw [h]; simp
  contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case pos =>
  rw [r] at hp0
  have : m * d = 0 := by rw [h]; simp
  contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
rw [r] at hp0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
have : m * d = 0 := by rw [h]; simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m * d = 0
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
⊢ m * 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
hp0 : m * d ≠ 0
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : d = 0
this : m * d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
contradiction
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case neg =>
  rw [r] at h'
  have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
  exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
case neg =>
  rw [r] at h'
  have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
  exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : p ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
rw [r] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
have : d * m ≤ d * 1 := by simpa [mul_comm] using h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
⊢ d * m ≤ d * 1
[PROOFSTEP]
simpa [mul_comm] using h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p m : Associates α
hp0 : p ≠ 0
left✝ : ¬IsUnit p
h✝ : ∀ (a b : Associates α), p ∣ a * b → p ∣ a ∨ p ∣ b
d : Associates α
r : p = m * d
dvd_rfl' : p ∣ m * d
h' : m * d ∣ d
h : ¬d = 0
this : d * m ≤ d * 1
⊢ m = 1 ∨ m = m * d
[PROOFSTEP]
exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : Associates α
⊢ p ≤ 1 ↔ p = 1
[PROOFSTEP]
rw [← Associates.bot_eq_one, le_bot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
h : DvdNotUnit p q
hq : Irreducible q
⊢ IsUnit p
[PROOFSTEP]
obtain ⟨_, x, hx, hx'⟩ := h
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
hq : Irreducible q
left✝ : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p
[PROOFSTEP]
exact Or.resolve_right ((irreducible_iff.1 hq).right p x hx') hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p q : α
hp : DvdNotUnit p q
⊢ ¬IsUnit q
[PROOFSTEP]
obtain ⟨-, x, hx, rfl⟩ := hp
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (p * x)
[PROOFSTEP]
exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p q r : α
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r
[PROOFSTEP]
obtain ⟨u, rfl⟩ := Associated.symm h'
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h : DvdNotUnit p (r * ↑u)
h' : r * ↑u ~ᵤ r
⊢ DvdNotUnit p r
[PROOFSTEP]
obtain ⟨hp, x, hx⟩ := h
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ DvdNotUnit p r
[PROOFSTEP]
refine' ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
p r : α
u : αˣ
h' : r * ↑u ~ᵤ r
hp : p ≠ 0
x : α
hx : ¬IsUnit x ∧ r * ↑u = p * x
⊢ r = p * (x * ↑u⁻¹)
[PROOFSTEP]
rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p b : α
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b
[PROOFSTEP]
cases' h with a ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ IsUnit b
[PROOFSTEP]
refine' isUnit_of_mul_eq_one b a ((mul_right_inj' hp).mp _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p b : α
hp : p ≠ 0
a : αˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1
[PROOFSTEP]
rwa [← mul_assoc, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
⊢ ¬p ~ᵤ q
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
h : DvdNotUnit p (p * ↑a)
⊢ False
[PROOFSTEP]
obtain ⟨hp, x, hx, hx'⟩ := h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
x : α
hx : ¬IsUnit x
hx' : p * ↑a = p * x
⊢ False
[PROOFSTEP]
rcases(mul_right_inj' hp).mp hx' with rfl
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
a : αˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False
[PROOFSTEP]
exact hx a.isUnit
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
⊢ p ≠ q
[PROOFSTEP]
by_contra hcontra
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
h : DvdNotUnit p q
hcontra : p = q
⊢ False
[PROOFSTEP]
obtain ⟨hp, x, hx', hx''⟩ := h
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False
[PROOFSTEP]
conv_lhs at hx'' => rw [← hcontra, ← mul_one p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
| q
[PROOFSTEP]
rw [← hcontra, ← mul_one p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
| q
[PROOFSTEP]
rw [← hcontra, ← mul_one p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : q = p * x
| q
[PROOFSTEP]
rw [← hcontra, ← mul_one p]
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit x
hx'' : p * 1 = p * x
⊢ False
[PROOFSTEP]
rw [(mul_left_cancel₀ hp hx'').symm] at hx'
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hcontra : p = q
hp : p ≠ 0
x : α
hx' : ¬IsUnit 1
hx'' : p * 1 = p * x
⊢ False
[PROOFSTEP]
exact hx' isUnit_one
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective fun n => q ^ n
[PROOFSTEP]
refine' injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))
[PROOFSTEP]
exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
q : α
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
[PROOFSTEP]
exact (pow_mul_pow_sub q h.le).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q : α
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
induction' n with n ih generalizing q
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
q : α
⊢ q ∣ p ^ Nat.zero ↔ ∃ i, i ≤ Nat.zero ∧ q ~ᵤ p ^ i
[PROOFSTEP]
simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
⊢ q ∣ p ^ Nat.succ n ↔ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p ^ Nat.succ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
rw [pow_succ] at h
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
[GOAL]
case succ.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : p * q ∣ p * p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
[PROOFSTEP]
rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
[GOAL]
case succ.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
[PROOFSTEP]
rcases h with ⟨i, hi, hq⟩
[GOAL]
case succ.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ p * q ~ᵤ p ^ i
[PROOFSTEP]
refine' ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans _⟩
[GOAL]
case succ.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p ^ (i + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ p * p ^ i ~ᵤ p * p ^ i
[PROOFSTEP]
rfl
[GOAL]
case succ.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
obtain ⟨i, hi, hq⟩ := ih.mp hno
[GOAL]
case succ.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p q✝ : α
hp : Prime p
n : ℕ
ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : α
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ Nat.succ n ∧ q ~ᵤ p ^ i
[PROOFSTEP]
exact ⟨i, hi.trans n.le_succ, hq⟩