[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
⊢ ¬IsUnit p
[PROOFSTEP]
simpa only [Associates.isUnit_iff_eq_one] using hp.1
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = a * b
ha : a = p
⊢ IsUnit b
[PROOFSTEP]
rw [ha] at h 
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ IsUnit b
[PROOFSTEP]
apply isUnit_of_associated_mul (show Associated (p * b) p by conv_rhs => rw [h]) h₁
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ Associated (p * b) p
[PROOFSTEP]
conv_rhs => rw [h]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
| p
[PROOFSTEP]
rw [h]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
| p
[PROOFSTEP]
rw [h]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
| p
[PROOFSTEP]
rw [h]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
⊢ p ≠ ⊥
[PROOFSTEP]
simpa only [Associates.isUnit_iff_eq_one, Associates.bot_eq_one] using hp.1
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb✝ : ¬p ∣ b
hb : IsUnit b
⊢ b = ⊥
[PROOFSTEP]
rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb 
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * ↑(IsUnit.unit ha)⁻¹
[PROOFSTEP]
simp [hab]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * a * ↑(IsUnit.unit ha)⁻¹
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * (a * ↑(IsUnit.unit ha)⁻¹)
[PROOFSTEP]
rw [IsUnit.mul_val_inv ha]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = b * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ∃ c, c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ i, r = c i
[PROOFSTEP]
refine' ⟨fun i => p ^ (i : ℕ), _, fun n m h => _, @fun y => ⟨fun h => _, _⟩⟩
[GOAL]
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ (fun i => p ^ ↑i) 1 = p
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p
[PROOFSTEP]
rw [Fin.val_one', Nat.mod_eq_of_lt, pow_one]
[GOAL]
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1
[PROOFSTEP]
exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)
[GOAL]
case refine'_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n✝ : ℕ
hn : n✝ ≠ 0
hp : Prime p
n m : Fin (n✝ + 1)
h : n < m
⊢ (fun i => p ^ ↑i) n < (fun i => p ^ ↑i) m
[PROOFSTEP]
exact
  Associates.dvdNotUnit_iff_lt.mp
    ⟨pow_ne_zero n hp.ne_zero, p ^ (m - n : ℕ),
      not_isUnit_of_not_isUnit_dvd hp.not_unit (dvd_pow dvd_rfl (Nat.sub_pos_of_lt h).ne'),
      (pow_mul_pow_sub p h.le).symm⟩
[GOAL]
case refine'_3
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
⊢ ∃ i, y = (fun i => p ^ ↑i) i
[PROOFSTEP]
obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h
[GOAL]
case refine'_3.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : Associated y (p ^ i)
⊢ ∃ i, y = (fun i => p ^ ↑i) i
[PROOFSTEP]
rw [associated_iff_eq] at hi 
[GOAL]
case refine'_3.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
h : y ≤ p ^ n
i : ℕ
i_le : i ≤ n
hi : y = p ^ i
⊢ ∃ i, y = (fun i => p ^ ↑i) i
[PROOFSTEP]
exact ⟨⟨i, Nat.lt_succ_of_le i_le⟩, hi⟩
[GOAL]
case refine'_4
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
y : Associates M
⊢ (∃ i, y = (fun i => p ^ ↑i) i) → y ≤ p ^ n
[PROOFSTEP]
rintro ⟨i, rfl⟩
[GOAL]
case refine'_4.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
i : Fin (n + 1)
⊢ (fun i => p ^ ↑i) i ≤ p ^ n
[PROOFSTEP]
exact ⟨p ^ (n - i : ℕ), (pow_mul_pow_sub p (Nat.succ_le_succ_iff.mp i.2)).symm⟩
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ IsUnit (c 0)
[PROOFSTEP]
obtain ⟨i, hr⟩ := h₂.mp Associates.one_le
[GOAL]
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ IsUnit (c 0)
[PROOFSTEP]
rw [Associates.isUnit_iff_eq_one, ← Associates.le_one_iff, hr]
[GOAL]
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ c i
[PROOFSTEP]
exact h₁.monotone (Fin.zero_le i)
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
⊢ Irreducible (c 1)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
hn : Nat.zero ≠ 0
c : Fin (Nat.zero + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ Irreducible (c 1)
[PROOFSTEP]
contradiction
[GOAL]
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ Irreducible (c 1)
[PROOFSTEP]
refine' (Associates.isAtom_iff (ne_zero_of_dvd_ne_zero hq (h₂.2 ⟨1, rfl⟩))).mp ⟨_, fun b hb => _⟩
[GOAL]
case succ.refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ c 1 ≠ ⊥
[PROOFSTEP]
exact ne_bot_of_gt (h₁ (show (0 : Fin (n + 2)) < 1 from Fin.one_pos))
[GOAL]
case succ.refine'_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
b : Associates M
hb : b < c 1
⊢ b = ⊥
[PROOFSTEP]
obtain ⟨⟨i, hi⟩, rfl⟩ := h₂.1 (hb.le.trans (h₂.2 ⟨1, rfl⟩))
[GOAL]
case succ.refine'_2.intro.mk
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : ℕ
hi : i < Nat.succ n + 1
hb : c { val := i, isLt := hi } < c 1
⊢ c { val := i, isLt := hi } = ⊥
[PROOFSTEP]
cases i
[GOAL]
case succ.refine'_2.intro.mk.zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : Nat.zero < Nat.succ n + 1
hb : c { val := Nat.zero, isLt := hi } < c 1
⊢ c { val := Nat.zero, isLt := hi } = ⊥
[PROOFSTEP]
exact (Associates.isUnit_iff_eq_one _).mp (first_of_chain_isUnit h₁ @h₂)
[GOAL]
case succ.refine'_2.intro.mk.succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
n✝ : ℕ
hi : Nat.succ n✝ < Nat.succ n + 1
hb : c { val := Nat.succ n✝, isLt := hi } < c 1
⊢ c { val := Nat.succ n✝, isLt := hi } = ⊥
[PROOFSTEP]
simpa [Fin.lt_iff_val_lt_val] using h₁.lt_iff_lt.mp hb
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
⊢ p = c 1
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
hn : Nat.zero ≠ 0
c : Fin (Nat.zero + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ p = c 1
[PROOFSTEP]
contradiction
[GOAL]
case succ
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ p = c 1
[PROOFSTEP]
obtain ⟨i, rfl⟩ := h₂.1 (dvd_trans hp' hr)
[GOAL]
case succ.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (Nat.succ n + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ c i = c 1
[PROOFSTEP]
refine' congr_arg c (eq_of_ge_of_not_gt _ fun hi => _)
[GOAL]
case succ.intro.refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (Nat.succ n + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ 1 ≤ i
[PROOFSTEP]
rw [Fin.le_iff_val_le_val, Fin.val_one, Nat.succ_le_iff, ← Fin.val_zero' (n.succ + 1), ← Fin.lt_iff_val_lt_val,
  Fin.pos_iff_ne_zero]
[GOAL]
case succ.intro.refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (Nat.succ n + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case succ.intro.refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hp : Prime (c 0)
hp' : c 0 ∣ r
⊢ False
[PROOFSTEP]
exact hp.not_unit (first_of_chain_isUnit h₁ @h₂)
[GOAL]
case succ.intro.refine'_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (Nat.succ n + 1)
hp : Prime (c i)
hp' : c i ∣ r
hi : 1 < i
⊢ False
[PROOFSTEP]
obtain rfl | ⟨j, rfl⟩ := i.eq_zero_or_eq_succ
[GOAL]
case succ.intro.refine'_2.inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hp : Prime (c 0)
hp' : c 0 ∣ r
hi : 1 < 0
⊢ False
[PROOFSTEP]
cases hi
[GOAL]
case succ.intro.refine'_2.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c (Fin.succ j))
hp' : c (Fin.succ j) ∣ r
hi : 1 < Fin.succ j
⊢ False
[PROOFSTEP]
refine'
  not_irreducible_of_not_unit_dvdNotUnit
    (DvdNotUnit.not_unit (Associates.dvdNotUnit_iff_lt.2 (h₁ (show (0 : Fin (n + 2)) < j from _)))) _ hp.irreducible
[GOAL]
case succ.intro.refine'_2.inr.intro.refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c (Fin.succ j))
hp' : c (Fin.succ j) ∣ r
hi : 1 < Fin.succ j
⊢ 0 < ↑↑j
[PROOFSTEP]
simpa [Fin.succ_lt_succ_iff, Fin.lt_iff_val_lt_val] using hi
[GOAL]
case succ.intro.refine'_2.inr.intro.refine'_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c (Fin.succ j))
hp' : c (Fin.succ j) ∣ r
hi : 1 < Fin.succ j
⊢ DvdNotUnit (c ↑↑j) (c (Fin.succ j))
[PROOFSTEP]
refine' Associates.dvdNotUnit_iff_lt.2 (h₁ _)
[GOAL]
case succ.intro.refine'_2.inr.intro.refine'_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : Nat.succ n ≠ 0
c : Fin (Nat.succ n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c (Fin.succ j))
hp' : c (Fin.succ j) ∣ r
hi : 1 < Fin.succ j
⊢ ↑↑j < Fin.succ j
[PROOFSTEP]
simpa only [Fin.coe_eq_castSucc] using Fin.lt_succ
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
⊢ Finset.card m ≤ n + 1
[PROOFSTEP]
classical
have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c :=
  by
  intro r hr
  obtain ⟨i, hi⟩ := h₂.1 hr
  exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
rw [← Finset.card_fin (n + 1)]
exact (Finset.card_le_of_subset fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
⊢ Finset.card m ≤ n + 1
[PROOFSTEP]
have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c :=
  by
  intro r hr
  obtain ⟨i, hi⟩ := h₂.1 hr
  exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
⊢ ∀ (r : Associates M), r ≤ q → r ∈ Finset.image c Finset.univ
[PROOFSTEP]
intro r hr
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
r : Associates M
hr : r ≤ q
⊢ r ∈ Finset.image c Finset.univ
[PROOFSTEP]
obtain ⟨i, hi⟩ := h₂.1 hr
[GOAL]
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
r : Associates M
hr : r ≤ q
i : Fin (n + 1)
hi : r = c i
⊢ r ∈ Finset.image c Finset.univ
[PROOFSTEP]
exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
mem_image : ∀ (r : Associates M), r ≤ q → r ∈ Finset.image c Finset.univ
⊢ Finset.card m ≤ n + 1
[PROOFSTEP]
rw [← Finset.card_fin (n + 1)]
[GOAL]
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ (r : Associates M), r ∈ m → r ≤ q
mem_image : ∀ (r : Associates M), r ≤ q → r ∈ Finset.image c Finset.univ
⊢ Finset.card m ≤ Finset.card Finset.univ
[PROOFSTEP]
exact (Finset.card_le_of_subset fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
⊢ ∃ i, r = c 1 ^ ↑i
[PROOFSTEP]
classical
let i := Multiset.card (normalizedFactors r)
have hi : normalizedFactors r = Multiset.replicate i (c 1) :=
  by
  apply Multiset.eq_replicate_of_mem
  intro b hb
  refine'
    eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
      (dvd_of_mem_normalizedFactors hb)
have H : r = c 1 ^ i :=
  by
  have := UniqueFactorizationMonoid.normalizedFactors_prod (ne_zero_of_dvd_ne_zero hq hr)
  rw [associated_iff_eq, hi, Multiset.prod_replicate] at this 
  rw [this]
refine' ⟨⟨i, _⟩, H⟩
have : (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card = i + 1 :=
  by
  conv_rhs => rw [← Finset.card_fin (i + 1)]
  cases n
  · contradiction
  rw [Finset.card_image_iff]
  refine' Set.injOn_of_injective (fun m m' h => Fin.ext _) _
  refine' pow_injective_of_not_unit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) _ h
  exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q
· simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
  apply card_subset_divisors_le_length_of_chain (@h₂) H'
simp only [Finset.mem_image]
rintro r ⟨a, _, rfl⟩
refine' dvd_trans _ hr
use c 1 ^ (i - (a : ℕ))
rw [pow_mul_pow_sub (c 1)]
· exact H
· exact Nat.succ_le_succ_iff.mp a.2
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
⊢ ∃ i, r = c 1 ^ ↑i
[PROOFSTEP]
let i := Multiset.card (normalizedFactors r)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
⊢ ∃ i, r = c 1 ^ ↑i
[PROOFSTEP]
have hi : normalizedFactors r = Multiset.replicate i (c 1) :=
  by
  apply Multiset.eq_replicate_of_mem
  intro b hb
  refine'
    eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
      (dvd_of_mem_normalizedFactors hb)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
⊢ normalizedFactors r = Multiset.replicate i (c 1)
[PROOFSTEP]
apply Multiset.eq_replicate_of_mem
[GOAL]
case a
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
⊢ ∀ (b : Associates M), b ∈ normalizedFactors r → b = c 1
[PROOFSTEP]
intro b hb
[GOAL]
case a
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
b : Associates M
hb : b ∈ normalizedFactors r
⊢ b = c 1
[PROOFSTEP]
refine'
  eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
    (dvd_of_mem_normalizedFactors hb)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
⊢ ∃ i, r = c 1 ^ ↑i
[PROOFSTEP]
have H : r = c 1 ^ i :=
  by
  have := UniqueFactorizationMonoid.normalizedFactors_prod (ne_zero_of_dvd_ne_zero hq hr)
  rw [associated_iff_eq, hi, Multiset.prod_replicate] at this 
  rw [this]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
⊢ r = c 1 ^ i
[PROOFSTEP]
have := UniqueFactorizationMonoid.normalizedFactors_prod (ne_zero_of_dvd_ne_zero hq hr)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
this : Associated (Multiset.prod (normalizedFactors r)) r
⊢ r = c 1 ^ i
[PROOFSTEP]
rw [associated_iff_eq, hi, Multiset.prod_replicate] at this 
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
this : c 1 ^ i = r
⊢ r = c 1 ^ i
[PROOFSTEP]
rw [this]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ ∃ i, r = c 1 ^ ↑i
[PROOFSTEP]
refine' ⟨⟨i, _⟩, H⟩
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ i < n + 1
[PROOFSTEP]
have : (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card = i + 1 :=
  by
  conv_rhs => rw [← Finset.card_fin (i + 1)]
  cases n
  · contradiction
  rw [Finset.card_image_iff]
  refine' Set.injOn_of_injective (fun m m' h => Fin.ext _) _
  refine' pow_injective_of_not_unit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) _ h
  exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
[PROOFSTEP]
conv_rhs => rw [← Finset.card_fin (i + 1)]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| i + 1
[PROOFSTEP]
rw [← Finset.card_fin (i + 1)]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| i + 1
[PROOFSTEP]
rw [← Finset.card_fin (i + 1)]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| i + 1
[PROOFSTEP]
rw [← Finset.card_fin (i + 1)]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = Finset.card Finset.univ
[PROOFSTEP]
cases n
[GOAL]
case zero
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hn : Nat.zero ≠ 0
c : Fin (Nat.zero + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = Finset.card Finset.univ
[PROOFSTEP]
contradiction
[GOAL]
case succ
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
n✝ : ℕ
hn : Nat.succ n✝ ≠ 0
c : Fin (Nat.succ n✝ + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = Finset.card Finset.univ
[PROOFSTEP]
rw [Finset.card_image_iff]
[GOAL]
case succ
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
n✝ : ℕ
hn : Nat.succ n✝ ≠ 0
c : Fin (Nat.succ n✝ + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Set.InjOn (fun m => c 1 ^ ↑m) ↑Finset.univ
[PROOFSTEP]
refine' Set.injOn_of_injective (fun m m' h => Fin.ext _) _
[GOAL]
case succ
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
n✝ : ℕ
hn : Nat.succ n✝ ≠ 0
c : Fin (Nat.succ n✝ + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ ↑m = c 1 ^ ↑m'
⊢ ↑m = ↑m'
[PROOFSTEP]
refine' pow_injective_of_not_unit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) _ h
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
n✝ : ℕ
hn : Nat.succ n✝ ≠ 0
c : Fin (Nat.succ n✝ + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ ↑m = c 1 ^ ↑m'
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case succ
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
n✝ : ℕ
hn : Nat.succ n✝ ≠ 0
c : Fin (Nat.succ n✝ + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ ↑m = c 1 ^ ↑m'
⊢ c 1 ≠ 0
[PROOFSTEP]
exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
⊢ i < n + 1
[PROOFSTEP]
suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
H' : ∀ (r_1 : Associates M), r_1 ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ → r_1 ≤ q
⊢ i < n + 1
[PROOFSTEP]
simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
H' : ∀ (r_1 : Associates M), r_1 ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ → r_1 ≤ q
⊢ Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) ≤ n + 1
[PROOFSTEP]
apply card_subset_divisors_le_length_of_chain (@h₂) H'
[GOAL]
case H'
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
⊢ ∀ (r_1 : Associates M), r_1 ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ → r_1 ≤ q
[PROOFSTEP]
simp only [Finset.mem_image]
[GOAL]
case H'
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
⊢ ∀ (r_1 : Associates M), (∃ a, a ∈ Finset.univ ∧ c 1 ^ ↑a = r_1) → r_1 ≤ q
[PROOFSTEP]
rintro r ⟨a, _, rfl⟩
[GOAL]
case H'.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
a : Fin (↑Multiset.card (normalizedFactors r) + 1)
left✝ : a ∈ Finset.univ
⊢ c 1 ^ ↑a ≤ q
[PROOFSTEP]
refine' dvd_trans _ hr
[GOAL]
case H'.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
a : Fin (↑Multiset.card (normalizedFactors r) + 1)
left✝ : a ∈ Finset.univ
⊢ c 1 ^ ↑a ∣ r
[PROOFSTEP]
use c 1 ^ (i - (a : ℕ))
[GOAL]
case h
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
a : Fin (↑Multiset.card (normalizedFactors r) + 1)
left✝ : a ∈ Finset.univ
⊢ r = c 1 ^ ↑a * c 1 ^ (i - ↑a)
[PROOFSTEP]
rw [pow_mul_pow_sub (c 1)]
[GOAL]
case h
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
a : Fin (↑Multiset.card (normalizedFactors r) + 1)
left✝ : a ∈ Finset.univ
⊢ r = c 1 ^ i
[PROOFSTEP]
exact H
[GOAL]
case h
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : (fun x => ℕ) (normalizedFactors r) := ↑Multiset.card (normalizedFactors r)
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card (Finset.image (fun m => c 1 ^ ↑m) Finset.univ) = i + 1
a : Fin (↑Multiset.card (normalizedFactors r) + 1)
left✝ : a ∈ Finset.univ
⊢ ↑a ≤ i
[PROOFSTEP]
exact Nat.succ_le_succ_iff.mp a.2
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
⊢ q = c 1 ^ n
[PROOFSTEP]
classical
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq
convert hi'
refine' (Nat.lt_succ_iff.1 i.prop).antisymm' (Nat.le_of_succ_le_succ _)
calc
  n + 1 = (Finset.univ : Finset (Fin (n + 1))).card := (Finset.card_fin _).symm
  _ = (Finset.univ.image c).card := (Finset.card_image_iff.mpr (h₁.injective.injOn _)).symm
  _ ≤ (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card := (Finset.card_le_of_subset ?_)
  _ ≤ (Finset.univ : Finset (Fin (i + 1))).card := Finset.card_image_le
  _ = i + 1 := Finset.card_fin _
intro r hr
obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr
have := h₂.2 ⟨j, rfl⟩
rw [hi'] at this 
have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this
rcases h with ⟨u, hu, hu'⟩
refine' Finset.mem_image.mpr ⟨u, Finset.mem_univ _, _⟩
· rw [associated_iff_eq] at hu' 
  rw [Fin.val_cast_of_lt (Nat.lt_succ_of_le hu), hu']
· rw [← irreducible_iff_prime]
  exact second_of_chain_is_irreducible hn h₁ (@h₂) hq
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
⊢ q = c 1 ^ n
[PROOFSTEP]
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq
[GOAL]
case intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ q = c 1 ^ n
[PROOFSTEP]
convert hi'
[GOAL]
case h.e'_3.h.e'_6
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ n = ↑i
[PROOFSTEP]
refine' (Nat.lt_succ_iff.1 i.prop).antisymm' (Nat.le_of_succ_le_succ _)
[GOAL]
case h.e'_3.h.e'_6
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ Nat.succ n ≤ Nat.succ ↑i
[PROOFSTEP]
calc
  n + 1 = (Finset.univ : Finset (Fin (n + 1))).card := (Finset.card_fin _).symm
  _ = (Finset.univ.image c).card := (Finset.card_image_iff.mpr (h₁.injective.injOn _)).symm
  _ ≤ (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card := (Finset.card_le_of_subset ?_)
  _ ≤ (Finset.univ : Finset (Fin (i + 1))).card := Finset.card_image_le
  _ = i + 1 := Finset.card_fin _
[GOAL]
case h.e'_3.h.e'_6
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
⊢ Finset.image c Finset.univ ⊆ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
[PROOFSTEP]
intro r hr
[GOAL]
case h.e'_3.h.e'_6
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
r : Associates M
hr : r ∈ Finset.image c Finset.univ
⊢ r ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
[PROOFSTEP]
obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr
[GOAL]
case h.e'_3.h.e'_6.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
[PROOFSTEP]
have := h₂.2 ⟨j, rfl⟩
[GOAL]
case h.e'_3.h.e'_6.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ q
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
[PROOFSTEP]
rw [hi'] at this 
[GOAL]
case h.e'_3.h.e'_6.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
[PROOFSTEP]
have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_2
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
h : ∃ i_1, i_1 ≤ ↑i ∧ Associated (c j) (c 1 ^ i_1)
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
case h.e'_3.h.e'_6.intro.intro.refine_1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)
[PROOFSTEP]
rcases h with ⟨u, hu, hu'⟩
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_2.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
u : ℕ
hu : u ≤ ↑i
hu' : Associated (c j) (c 1 ^ u)
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ
case h.e'_3.h.e'_6.intro.intro.refine_1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)
[PROOFSTEP]
refine' Finset.mem_image.mpr ⟨u, Finset.mem_univ _, _⟩
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_2.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
u : ℕ
hu : u ≤ ↑i
hu' : Associated (c j) (c 1 ^ u)
⊢ c 1 ^ ↑↑u = c j
[PROOFSTEP]
rw [associated_iff_eq] at hu' 
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_2.intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
u : ℕ
hu : u ≤ ↑i
hu' : c j = c 1 ^ u
⊢ c 1 ^ ↑↑u = c j
[PROOFSTEP]
rw [Fin.val_cast_of_lt (Nat.lt_succ_of_le hu), hu']
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)
[PROOFSTEP]
rw [← irreducible_iff_prime]
[GOAL]
case h.e'_3.h.e'_6.intro.intro.refine_1
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Irreducible (c 1)
[PROOFSTEP]
exact second_of_chain_is_irreducible hn h₁ (@h₂) hq
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
[PROOFSTEP]
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
[PROOFSTEP]
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑(↑d { val := 1, property := (_ : 1 ∣ m) }) = 1
[PROOFSTEP]
simp only [← Associates.bot_eq_one, Subtype.mk_bot, bot_le, Subtype.coe_eq_bot_iff]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ ↑d ⊥ = ⊥
[PROOFSTEP]
letI : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) _ _ := OrderIsoClass.toBotHomClass
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m : Associates M
n : Associates N
d : { l // l ≤ m } ≃o { l // l ≤ n }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : BotHomClass ({ l // l ≤ m } ≃o { l // l ≤ n }) { l // l ≤ m } { l // l ≤ n } := OrderIsoClass.toBotHomClass
⊢ ↑d ⊥ = ⊥
[PROOFSTEP]
exact map_bot d
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ u = 1
[PROOFSTEP]
rw [show u = (d.symm ⟨d ⟨u, hu'⟩, (d ⟨u, hu'⟩).prop⟩) by
    simp only [Subtype.coe_eta, OrderIso.symm_apply_apply, Subtype.coe_mk]]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ u =
    ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) })
[PROOFSTEP]
simp only [Subtype.coe_eta, OrderIso.symm_apply_apply, Subtype.coe_mk]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    1
[PROOFSTEP]
conv_rhs => rw [← factor_orderIso_map_one_eq_bot d.symm]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d.symm]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d.symm]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d.symm]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : ↑(↑d { val := u, property := hu' }) = 1
⊢ ↑(↑(OrderIso.symm d)
        { val := ↑(↑d { val := u, property := hu' }),
          property := (_ : ↑(↑d { val := u, property := hu' }) ∈ Set.Iic n) }) =
    ↑(↑(OrderIso.symm d) { val := 1, property := (_ : 1 ∣ n) })
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(↑d { val := u, property := hu' }) = 1
[PROOFSTEP]
simp_rw [hu]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
⊢ ↑(↑d { val := 1, property := (_ : (fun x => x ∈ Set.Iic m) 1) }) = 1
[PROOFSTEP]
conv_rhs => rw [← factor_orderIso_map_one_eq_bot d]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d]
[GOAL]
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
N : Type u_2
inst✝ : CancelCommMonoidWithZero N
m u : Associates M
n : Associates N
hu' : u ≤ m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hu : u = 1
| 1
[PROOFSTEP]
rw [← factor_orderIso_map_one_eq_bot d]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
[PROOFSTEP]
by_cases hs : s = 0
[GOAL]
case pos
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
[PROOFSTEP]
simp [hs]
[GOAL]
case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
[PROOFSTEP]
suffices (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s = (d ⟨p ^ s, hs'⟩)
  by
  rw [this]
  apply Subtype.prop (d ⟨p ^ s, hs'⟩)
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s ≤ n
[PROOFSTEP]
rw [this]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
this : ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
⊢ ↑(↑d { val := p ^ s, property := hs' }) ≤ n
[PROOFSTEP]
apply Subtype.prop (d ⟨p ^ s, hs'⟩)
[GOAL]
case neg
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs' : p ^ s ≤ m
hs : ¬s = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ s = ↑(↑d { val := p ^ s, property := hs' })
[PROOFSTEP]
obtain ⟨c₁, rfl, hc₁', hc₁''⟩ := exists_chain_of_prime_pow hs (prime_of_normalized_factor p hp)
[GOAL]
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
let c₂ : Fin (s + 1) → Associates N := fun t => d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
t : Fin (s + 1)
⊢ c₁ t = c₁ t
[PROOFSTEP]
simp
[GOAL]
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
have c₂_def : ∀ t, c₂ t = d ⟨c₁ t, _⟩ := fun t => rfl
[GOAL]
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1, property := (_ : c₁ 1 ∣ m) }) ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
rw [← c₂_def]
[GOAL]
case neg.intro.intro.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ c₂ 1 ^ s = ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
refine' (eq_pow_second_of_chain_of_has_chain hs (fun t u h => _) (@fun r => ⟨@fun hr => _, _⟩) _).symm
[GOAL]
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ c₂ t < c₂ u
[PROOFSTEP]
rw [c₂_def, c₂_def, Subtype.coe_lt_coe, d.lt_iff_lt, Subtype.mk_lt_mk, hc₁'.lt_iff_lt]
[GOAL]
case neg.intro.intro.intro.refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
t u : Fin (s + 1)
h : t < u
⊢ t < u
[PROOFSTEP]
exact h
[GOAL]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
⊢ ∃ i, r = c₂ i
[PROOFSTEP]
have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2
[GOAL]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ∃ i, r = c₂ i
[PROOFSTEP]
suffices d.symm ⟨r, this⟩ ≤ ⟨c₁ 1 ^ s, hs'⟩ by
  obtain ⟨i, hi⟩ := hc₁''.1 this
  use i
  simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
⊢ ∃ i, r = c₂ i
[PROOFSTEP]
obtain ⟨i, hi⟩ := hc₁''.1 this
[GOAL]
case intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ ∃ i, r = c₂ i
[PROOFSTEP]
use i
[GOAL]
case h
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this✝ : r ≤ n
this : ↑(OrderIso.symm d) { val := r, property := this✝ } ≤ { val := c₁ 1 ^ s, property := hs' }
i : Fin (s + 1)
hi : ↑(↑(OrderIso.symm d) { val := r, property := this✝ }) = c₁ i
⊢ r = c₂ i
[PROOFSTEP]
simp only [c₂_def, ← hi, d.apply_symm_apply, Subtype.coe_eta, Subtype.coe_mk]
[GOAL]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
conv_rhs => rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
| { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
| { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
| { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
rw [← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩]
[GOAL]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ ↑(OrderIso.symm d) { val := r, property := this } ≤ ↑(OrderIso.symm d) (↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
rw [d.symm.le_iff_le]
[GOAL]
case neg.intro.intro.intro.refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
hr : r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
this : r ≤ n
⊢ { val := r, property := this } ≤ ↑d { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
simpa only [← Subtype.coe_le_coe, Subtype.coe_mk] using hr
[GOAL]
case neg.intro.intro.intro.refine'_3
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
⊢ (∃ i, r = c₂ i) → r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
rintro ⟨i, hr⟩
[GOAL]
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ r ≤ ↑(↑d { val := c₁ 1 ^ s, property := hs' })
[PROOFSTEP]
rw [hr, c₂_def, Subtype.coe_le_coe, d.le_iff_le]
[GOAL]
case neg.intro.intro.intro.refine'_3.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
r : Associates N
i : Fin (s + 1)
hr : r = c₂ i
⊢ { val := c₁ i, property := (_ : c₁ i ≤ m) } ≤ { val := c₁ 1 ^ s, property := hs' }
[PROOFSTEP]
simpa [Subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩
[GOAL]
case neg.intro.intro.intro.refine'_4
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t => ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(↑d { val := c₁ t, property := (_ : c₁ t ≤ m) })
⊢ ↑(↑d { val := c₁ 1 ^ s, property := hs' }) ≠ 0
[PROOFSTEP]
exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Prime ↑(↑d { val := p, property := (_ : p ∣ m) })
[PROOFSTEP]
rw [← irreducible_iff_prime]
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ Irreducible ↑(↑d { val := p, property := (_ : p ∣ m) })
[PROOFSTEP]
refine' (Associates.isAtom_iff <| ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨_, fun b hb => _⟩
[GOAL]
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ≠ ⊥
[PROOFSTEP]
rw [Ne.def, ← Associates.isUnit_iff_eq_bot, Associates.isUnit_iff_eq_one, coe_factor_orderIso_map_eq_one_iff _ d]
[GOAL]
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ¬p = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hp : 1 ∈ normalizedFactors m
⊢ False
[PROOFSTEP]
exact (prime_of_normalized_factor 1 hp).not_unit isUnit_one
[GOAL]
case refine'_2
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
⊢ b = ⊥
[PROOFSTEP]
obtain ⟨x, hx⟩ := d.surjective ⟨b, le_trans (le_of_lt hb) (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop⟩
[GOAL]
case refine'_2.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
[PROOFSTEP]
rw [← Subtype.coe_mk b _, ← hx] at hb 
[GOAL]
case refine'_2.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
⊢ b = ⊥
[PROOFSTEP]
letI : OrderBot { l : Associates M // l ≤ m } := Subtype.orderBot bot_le
[GOAL]
case refine'_2.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
⊢ b = ⊥
[PROOFSTEP]
letI : OrderBot { l : Associates N // l ≤ n } := Subtype.orderBot bot_le
[GOAL]
case refine'_2.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ b = ⊥
[PROOFSTEP]
suffices x = ⊥ by
  rw [this, OrderIso.map_bot d] at hx 
  refine' (Subtype.mk_eq_bot_iff _ _).mp hx.symm
  simp
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ b = ⊥
[PROOFSTEP]
rw [this, OrderIso.map_bot d] at hx 
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ b = ⊥
[PROOFSTEP]
refine' (Subtype.mk_eq_bot_iff _ _).mp hx.symm
[GOAL]
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ⊥ = { val := b, property := (_ : b ≤ n) }
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
this : x = ⊥
⊢ ⊥ ∈ Set.Iic n
[PROOFSTEP]
simp
[GOAL]
case refine'_2.intro
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
x : ↑(Set.Iic m)
hb : ↑(↑d x) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d x = { val := b, property := (_ : b ≤ n) }
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
⊢ x = ⊥
[PROOFSTEP]
obtain ⟨a, ha⟩ := x
[GOAL]
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ { val := a, property := ha } = ⊥
[PROOFSTEP]
rw [Subtype.mk_eq_bot_iff]
[GOAL]
case refine'_2.intro.mk
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ a = ⊥
[PROOFSTEP]
exact
  ((Associates.isAtom_iff <| Prime.ne_zero <| prime_of_normalized_factor p hp).mpr <|
        irreducible_of_normalized_factor p hp).right
    a (Subtype.mk_lt_mk.mp <| d.lt_iff_lt.mp hb)
[GOAL]
case refine'_2.intro.mk.hbot
M : Type u_1
inst✝⁴ : CancelCommMonoidWithZero M
N : Type u_2
inst✝³ : CancelCommMonoidWithZero N
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
hb✝ : b < ↑(↑d { val := p, property := (_ : p ∣ m) })
this✝ : OrderBot { l // l ≤ m } := Subtype.orderBot (_ : ⊥ ≤ m)
this : OrderBot { l // l ≤ n } := Subtype.orderBot (_ : ⊥ ≤ n)
a : Associates M
ha : a ∈ Set.Iic m
hb : ↑(↑d { val := a, property := ha }) < ↑(↑d { val := p, property := (_ : p ∣ m) })
hx : ↑d { val := a, property := ha } = { val := b, property := (_ : b ≤ n) }
⊢ ⊥ ∈ Set.Iic m
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd hn (map_prime_of_factor_orderIso hn hp d).irreducible
    (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).prop
[GOAL]
case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(↑d { val := p, property := (_ : p ∣ m) })) q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
rw [associated_iff_eq] at hq' 
[GOAL]
case intro.intro
M : Type u_1
inst✝⁵ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁴ : CancelCommMonoidWithZero N
inst✝³ : UniqueFactorizationMonoid N
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : DecidableEq (Associates M)
inst✝ : DecidableEq (Associates N)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
q : Associates N
hq : q ∈ normalizedFactors n
hq' : ↑(↑d { val := p, property := (_ : p ∣ m) }) = q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
rwa [hq']
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
simp [hm] at hp 
[GOAL]
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ multiplicity p m ≤ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
rw [← PartENat.natCast_get (finite_iff_dom.1 <| finite_prime_left (prime_of_normalized_factor p hp) hm), ←
  pow_dvd_iff_le_multiplicity]
[GOAL]
case neg
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ^ Part.get (multiplicity p m) (_ : (multiplicity p m).Dom) ∣ n
[PROOFSTEP]
exact pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd _)
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ multiplicity p m = multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
refine' le_antisymm (multiplicity_prime_le_multiplicity_image_by_factor_orderIso hp d) _
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤ multiplicity p m
[PROOFSTEP]
suffices
  multiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n ≤
    multiplicity (↑(d.symm (d ⟨p, dvd_of_mem_normalizedFactors hp⟩))) m
  by
  rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this 
  exact this
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this :
  multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤
    multiplicity (↑(↑(OrderIso.symm d) (↑d { val := p, property := (_ : p ∣ m) }))) m
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤ multiplicity p m
[PROOFSTEP]
rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalizedFactors hp⟩, Subtype.coe_mk] at this 
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this :
  multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤ multiplicity (↑{ val := p, property := (_ : p ∣ m) }) m
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤ multiplicity p m
[PROOFSTEP]
exact this
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤
    multiplicity (↑(↑(OrderIso.symm d) (↑d { val := p, property := (_ : p ∣ m) }))) m
[PROOFSTEP]
letI := Classical.decEq (Associates N)
[GOAL]
M : Type u_1
inst✝⁶ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁵ : CancelCommMonoidWithZero N
inst✝⁴ : UniqueFactorizationMonoid N
inst✝³ : UniqueFactorizationMonoid M
inst✝² : DecidableRel fun x x_1 => x ∣ x_1
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableEq (Associates M)
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
this : DecidableEq (Associates N) := Classical.decEq (Associates N)
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n ≤
    multiplicity (↑(↑(OrderIso.symm d) (↑d { val := p, property := (_ : p ∣ m) }))) m
[PROOFSTEP]
simpa only [Subtype.coe_eta] using
  multiplicity_prime_le_multiplicity_image_by_factor_orderIso
    (mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors hn hp d) d.symm
[GOAL]
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
l : ↑(Set.Iic (Associates.mk m))
⊢ ↑associatesEquivOfUniqueUnits ↑l ∣ m
[PROOFSTEP]
obtain ⟨x, hx⟩ := l
[GOAL]
case mk
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x : Associates M
hx : x ∈ Set.Iic (Associates.mk m)
⊢ ↑associatesEquivOfUniqueUnits ↑{ val := x, property := hx } ∣ m
[PROOFSTEP]
rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
[GOAL]
case mk
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x : Associates M
hx : x ∈ Set.Iic (Associates.mk m)
⊢ x ≤ Associates.mk m
[PROOFSTEP]
exact hx
[GOAL]
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
l : ↑(Set.Iic (Associates.mk n))
⊢ ↑associatesEquivOfUniqueUnits ↑l ∣ n
[PROOFSTEP]
obtain ⟨x, hx⟩ := l
[GOAL]
case mk
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x : Associates N
hx : x ∈ Set.Iic (Associates.mk n)
⊢ ↑associatesEquivOfUniqueUnits ↑{ val := x, property := hx } ∣ n
[PROOFSTEP]
rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
[GOAL]
case mk
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x : Associates N
hx : x ∈ Set.Iic (Associates.mk n)
⊢ x ≤ Associates.mk n
[PROOFSTEP]
exact hx
[GOAL]
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x✝ : ↑(Set.Iic (Associates.mk m))
l : Associates M
hl : l ∈ Set.Iic (Associates.mk m)
⊢ (fun l =>
        {
          val :=
            Associates.mk
              ↑(↑d.symm
                  { val := ↑associatesEquivOfUniqueUnits ↑l, property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
          property :=
            (_ :
              Associates.mk
                  ↑(↑d.symm
                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                Associates.mk m) })
      ((fun l =>
          {
            val :=
              Associates.mk
                ↑(↑d
                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
            property :=
              (_ :
                Associates.mk
                    ↑(↑d
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                  Associates.mk n) })
        { val := l, property := hl }) =
    { val := l, property := hl }
[PROOFSTEP]
simp only [Subtype.coe_eta, Equiv.symm_apply_apply, Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, mk_out, out_mk,
  normalize_eq]
[GOAL]
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
x✝ : ↑(Set.Iic (Associates.mk n))
l : Associates N
hl : l ∈ Set.Iic (Associates.mk n)
⊢ (fun l =>
        {
          val :=
            Associates.mk
              ↑(↑d { val := ↑associatesEquivOfUniqueUnits ↑l, property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
          property :=
            (_ :
              Associates.mk
                  ↑(↑d
                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                Associates.mk n) })
      ((fun l =>
          {
            val :=
              Associates.mk
                ↑(↑d.symm
                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
            property :=
              (_ :
                Associates.mk
                    ↑(↑d.symm
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                  Associates.mk m) })
        { val := l, property := hl }) =
    { val := l, property := hl }
[PROOFSTEP]
simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_mk,
  normalize_eq, mk_out]
[GOAL]
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ∀ {a b : ↑(Set.Iic (Associates.mk m))},
    ↑{
              toFun := fun l =>
                {
                  val :=
                    Associates.mk
                      ↑(↑d
                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                  property :=
                    (_ :
                      Associates.mk
                          ↑(↑d
                              { val := ↑associatesEquivOfUniqueUnits ↑l,
                                property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                        Associates.mk n) },
              invFun := fun l =>
                {
                  val :=
                    Associates.mk
                      ↑(↑d.symm
                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                  property :=
                    (_ :
                      Associates.mk
                          ↑(↑d.symm
                              { val := ↑associatesEquivOfUniqueUnits ↑l,
                                property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                        Associates.mk m) },
              left_inv :=
                (_ :
                  ∀ (x : ↑(Set.Iic (Associates.mk m))),
                    (fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d.symm
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d.symm
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                  Associates.mk m) })
                        ((fun l =>
                            {
                              val :=
                                Associates.mk
                                  ↑(↑d
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                              property :=
                                (_ :
                                  Associates.mk
                                      ↑(↑d
                                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                    Associates.mk n) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : ↑(Set.Iic (Associates.mk n))),
                    (fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                  Associates.mk n) })
                        ((fun l =>
                            {
                              val :=
                                Associates.mk
                                  ↑(↑d.symm
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                              property :=
                                (_ :
                                  Associates.mk
                                      ↑(↑d.symm
                                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                    Associates.mk m) })
                          x) =
                      x) }
          a ≤
        ↑{
              toFun := fun l =>
                {
                  val :=
                    Associates.mk
                      ↑(↑d
                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                  property :=
                    (_ :
                      Associates.mk
                          ↑(↑d
                              { val := ↑associatesEquivOfUniqueUnits ↑l,
                                property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                        Associates.mk n) },
              invFun := fun l =>
                {
                  val :=
                    Associates.mk
                      ↑(↑d.symm
                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                  property :=
                    (_ :
                      Associates.mk
                          ↑(↑d.symm
                              { val := ↑associatesEquivOfUniqueUnits ↑l,
                                property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                        Associates.mk m) },
              left_inv :=
                (_ :
                  ∀ (x : ↑(Set.Iic (Associates.mk m))),
                    (fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d.symm
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d.symm
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                  Associates.mk m) })
                        ((fun l =>
                            {
                              val :=
                                Associates.mk
                                  ↑(↑d
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                              property :=
                                (_ :
                                  Associates.mk
                                      ↑(↑d
                                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                    Associates.mk n) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : ↑(Set.Iic (Associates.mk n))),
                    (fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                  Associates.mk n) })
                        ((fun l =>
                            {
                              val :=
                                Associates.mk
                                  ↑(↑d.symm
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                              property :=
                                (_ :
                                  Associates.mk
                                      ↑(↑d.symm
                                          { val := ↑associatesEquivOfUniqueUnits ↑l,
                                            property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                    Associates.mk m) })
                          x) =
                      x) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
N : Type u_2
inst✝² : CancelCommMonoidWithZero N
inst✝¹ : Unique Mˣ
inst✝ : Unique Nˣ
m : M
n : N
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
a : Associates M
ha : a ∈ Set.Iic (Associates.mk m)
b : Associates M
hb : b ∈ Set.Iic (Associates.mk m)
⊢ ↑{
            toFun := fun l =>
              {
                val :=
                  Associates.mk
                    ↑(↑d
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                property :=
                  (_ :
                    Associates.mk
                        ↑(↑d
                            { val := ↑associatesEquivOfUniqueUnits ↑l,
                              property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                      Associates.mk n) },
            invFun := fun l =>
              {
                val :=
                  Associates.mk
                    ↑(↑d.symm
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                property :=
                  (_ :
                    Associates.mk
                        ↑(↑d.symm
                            { val := ↑associatesEquivOfUniqueUnits ↑l,
                              property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                      Associates.mk m) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Set.Iic (Associates.mk m))),
                  (fun l =>
                        {
                          val :=
                            Associates.mk
                              ↑(↑d.symm
                                  { val := ↑associatesEquivOfUniqueUnits ↑l,
                                    property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                          property :=
                            (_ :
                              Associates.mk
                                  ↑(↑d.symm
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                Associates.mk m) })
                      ((fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                  Associates.mk n) })
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Set.Iic (Associates.mk n))),
                  (fun l =>
                        {
                          val :=
                            Associates.mk
                              ↑(↑d
                                  { val := ↑associatesEquivOfUniqueUnits ↑l,
                                    property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                          property :=
                            (_ :
                              Associates.mk
                                  ↑(↑d
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                Associates.mk n) })
                      ((fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d.symm
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d.symm
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                  Associates.mk m) })
                        x) =
                    x) }
        { val := a, property := ha } ≤
      ↑{
            toFun := fun l =>
              {
                val :=
                  Associates.mk
                    ↑(↑d
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                property :=
                  (_ :
                    Associates.mk
                        ↑(↑d
                            { val := ↑associatesEquivOfUniqueUnits ↑l,
                              property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                      Associates.mk n) },
            invFun := fun l =>
              {
                val :=
                  Associates.mk
                    ↑(↑d.symm
                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                property :=
                  (_ :
                    Associates.mk
                        ↑(↑d.symm
                            { val := ↑associatesEquivOfUniqueUnits ↑l,
                              property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                      Associates.mk m) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Set.Iic (Associates.mk m))),
                  (fun l =>
                        {
                          val :=
                            Associates.mk
                              ↑(↑d.symm
                                  { val := ↑associatesEquivOfUniqueUnits ↑l,
                                    property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                          property :=
                            (_ :
                              Associates.mk
                                  ↑(↑d.symm
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                Associates.mk m) })
                      ((fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                  Associates.mk n) })
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Set.Iic (Associates.mk n))),
                  (fun l =>
                        {
                          val :=
                            Associates.mk
                              ↑(↑d
                                  { val := ↑associatesEquivOfUniqueUnits ↑l,
                                    property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }),
                          property :=
                            (_ :
                              Associates.mk
                                  ↑(↑d
                                      { val := ↑associatesEquivOfUniqueUnits ↑l,
                                        property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ m) }) ≤
                                Associates.mk n) })
                      ((fun l =>
                          {
                            val :=
                              Associates.mk
                                ↑(↑d.symm
                                    { val := ↑associatesEquivOfUniqueUnits ↑l,
                                      property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }),
                            property :=
                              (_ :
                                Associates.mk
                                    ↑(↑d.symm
                                        { val := ↑associatesEquivOfUniqueUnits ↑l,
                                          property := (_ : ↑associatesEquivOfUniqueUnits ↑l ∣ n) }) ≤
                                  Associates.mk m) })
                        x) =
                    x) }
        { val := b, property := hb } ↔
    { val := a, property := ha } ≤ { val := b, property := hb }
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Associates.mk_le_mk_iff_dvd_iff, hd, Subtype.coe_mk,
  associatesEquivOfUniqueUnits_apply, out_dvd_iff, mk_out]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
suffices
  Prime
    (d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by simp [dvd_of_mem_normalizedFactors hp]⟩ :
      N)
  by
  simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq, associatesEquivOfUniqueUnits_symm_apply] at this 
  obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd hn this.irreducible
      (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert hp⟩).prop
  rwa [associated_iff_eq.mp hq']
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p) ∣ m
[PROOFSTEP]
simp [dvd_of_mem_normalizedFactors hp]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  Prime
    ↑(↑d
        { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
          property := (_ : p * 1 ∣ m) })
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
simp only [associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq, associatesEquivOfUniqueUnits_symm_apply] at this 
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this : Prime ↑(↑d { val := p, property := (_ : (fun l => l ∣ m) p) })
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd hn this.irreducible
    (d ⟨p, by apply dvd_of_mem_normalizedFactors; convert hp⟩).prop
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this : Prime ↑(↑d { val := p, property := (_ : (fun l => l ∣ m) p) })
⊢ p ∣ m
[PROOFSTEP]
apply dvd_of_mem_normalizedFactors
[GOAL]
case H
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this : Prime ↑(↑d { val := p, property := (_ : (fun l => l ∣ m) p) })
⊢ p ∈ normalizedFactors m
[PROOFSTEP]
convert hp
[GOAL]
case intro.intro
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this : Prime ↑(↑d { val := p, property := (_ : (fun l => l ∣ m) p) })
q : N
hq : q ∈ normalizedFactors n
hq' : Associated (↑(↑d { val := p, property := (_ : (fun l => l ∣ m) p) })) q
⊢ ↑(↑d { val := p, property := (_ : p ∣ m) }) ∈ normalizedFactors n
[PROOFSTEP]
rwa [associated_iff_eq.mp hq']
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ Prime
    ↑(↑d
        { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
          property := (_ : p * 1 ∣ m) })
[PROOFSTEP]
have :
  Associates.mk
      (d
          ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
            simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
              associatesEquivOfUniqueUnits_symm_apply]⟩ :
        N) =
    ↑(mkFactorOrderIsoOfFactorDvdEquiv hd
        ⟨associatesEquivOfUniqueUnits.symm p,
          by
          simp only [associatesEquivOfUniqueUnits_symm_apply]
          exact mk_dvd_mk.mpr (dvd_of_mem_normalizedFactors hp)⟩) :=
  by rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p) ∣ m
[PROOFSTEP]
simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq,
  associatesEquivOfUniqueUnits_symm_apply]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)
[PROOFSTEP]
simp only [associatesEquivOfUniqueUnits_symm_apply]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)
[PROOFSTEP]
exact mk_dvd_mk.mpr (dvd_of_mem_normalizedFactors hp)
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
[PROOFSTEP]
rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
⊢ Prime
    ↑(↑d
        { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
          property := (_ : p * 1 ∣ m) })
[PROOFSTEP]
rw [← Associates.prime_mk, this]
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
⊢ Prime
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
[PROOFSTEP]
letI := Classical.decEq (Associates M)
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ Prime
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
[PROOFSTEP]
refine' map_prime_of_factor_orderIso (mk_ne_zero.mpr hn) _ _
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ normalizedFactors (Associates.mk m)
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
    ((prime_mk p).mpr (prime_of_normalized_factor p (by convert hp))).irreducible
    (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
[GOAL]
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ p ∈ normalizedFactors ?m.1306674
[PROOFSTEP]
convert hp
[GOAL]
case intro.intro
M : Type u_1
inst✝⁷ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁶ : CancelCommMonoidWithZero N
inst✝⁵ : Unique Mˣ
inst✝⁴ : Unique Nˣ
inst✝³ : UniqueFactorizationMonoid M
inst✝² : UniqueFactorizationMonoid N
inst✝¹ : DecidableEq M
inst✝ : DecidableEq N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
q : Associates M
hq : q ∈ normalizedFactors (Associates.mk m)
hq' : Associated (Associates.mk p) q
⊢ ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ normalizedFactors (Associates.mk m)
[PROOFSTEP]
simpa only [associated_iff_eq.mp hq', associatesEquivOfUniqueUnits_symm_apply] using hq
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n = multiplicity p m
[PROOFSTEP]
apply Eq.symm
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ multiplicity p m = multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
suffices
  multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (Associates.mk
        ↑(d
            ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
              simp [dvd_of_mem_normalizedFactors hp]⟩))
      (Associates.mk n)
  by
  simpa only [multiplicity_mk_eq_multiplicity, associatesEquivOfUniqueUnits_symm_apply,
    associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p) ∣ m
[PROOFSTEP]
simp [dvd_of_mem_normalizedFactors hp]
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (Associates.mk
        ↑(↑d
            { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
              property := (_ : p * 1 ∣ m) }))
      (Associates.mk n)
⊢ multiplicity p m = multiplicity (↑(↑d { val := p, property := (_ : p ∣ m) })) n
[PROOFSTEP]
simpa only [multiplicity_mk_eq_multiplicity, associatesEquivOfUniqueUnits_symm_apply,
  associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq] using this
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (Associates.mk
        ↑(↑d
            { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
              property := (_ : p * 1 ∣ m) }))
      (Associates.mk n)
[PROOFSTEP]
have :
  Associates.mk
      (d
          ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), by
            simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply,
              associatesEquivOfUniqueUnits_apply, out_mk, normalize_eq]⟩ :
        N) =
    ↑(mkFactorOrderIsoOfFactorDvdEquiv hd
        ⟨associatesEquivOfUniqueUnits.symm p,
          by
          rw [associatesEquivOfUniqueUnits_symm_apply]
          exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)⟩) :=
  by rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p) ∣ m
[PROOFSTEP]
simp only [dvd_of_mem_normalizedFactors hp, associatesEquivOfUniqueUnits_symm_apply, associatesEquivOfUniqueUnits_apply,
  out_mk, normalize_eq]
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)
[PROOFSTEP]
rw [associatesEquivOfUniqueUnits_symm_apply]
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk p ∈ Set.Iic (Associates.mk m)
[PROOFSTEP]
exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)
[GOAL]
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
⊢ Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
[PROOFSTEP]
rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
⊢ multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (Associates.mk
        ↑(↑d
            { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
              property := (_ : p * 1 ∣ m) }))
      (Associates.mk n)
[PROOFSTEP]
rw [this]
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
⊢ multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
          { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
            property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) }))
      (Associates.mk n)
[PROOFSTEP]
letI := Classical.decEq (Associates M)
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ multiplicity (Associates.mk p) (Associates.mk m) =
    multiplicity
      (↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
          { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
            property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) }))
      (Associates.mk n)
[PROOFSTEP]
refine'
  multiplicity_prime_eq_multiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) _
    (mkFactorOrderIsoOfFactorDvdEquiv hd)
[GOAL]
case h
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
⊢ Associates.mk p ∈ normalizedFactors (Associates.mk m)
[PROOFSTEP]
obtain ⟨q, hq, hq'⟩ :=
  exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
    ((prime_mk p).mpr (prime_of_normalized_factor p hp)).irreducible (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
[GOAL]
case h.intro.intro
M : Type u_1
inst✝⁸ : CancelCommMonoidWithZero M
N : Type u_2
inst✝⁷ : CancelCommMonoidWithZero N
inst✝⁶ : Unique Mˣ
inst✝⁵ : Unique Nˣ
inst✝⁴ : UniqueFactorizationMonoid M
inst✝³ : UniqueFactorizationMonoid N
inst✝² : DecidableEq M
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : { l // l ∣ m } ≃ { l // l ∣ n }
hd : ∀ (l l' : { l // l ∣ m }), ↑(↑d l) ∣ ↑(↑d l') ↔ ↑l ∣ ↑l'
this✝ :
  Associates.mk
      ↑(↑d
          { val := ↑associatesEquivOfUniqueUnits (↑(MulEquiv.symm associatesEquivOfUniqueUnits) p),
            property := (_ : ↑normalize p ∣ m) }) =
    ↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd)
        { val := ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p,
          property := (_ : ↑(MulEquiv.symm associatesEquivOfUniqueUnits) p ∈ Set.Iic (Associates.mk m)) })
this : DecidableEq (Associates M) := Classical.decEq (Associates M)
q : Associates M
hq : q ∈ normalizedFactors (Associates.mk m)
hq' : Associated (Associates.mk p) q
⊢ Associates.mk p ∈ normalizedFactors (Associates.mk m)
[PROOFSTEP]
rwa [associated_iff_eq.mp hq']
