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
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
let i := Multiset.card (normalizedFactors r)
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
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
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)
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
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
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]
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
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
refine' ⟨⟨i, _⟩, 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
H' : ∀ (r_1 : Associates M), r_1 ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ → r_1 ≤ q
⊢ i < n + 1

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
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
suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q
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
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
simp only [Finset.mem_image]
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
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
rintro r ⟨a, _, rfl⟩
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
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
refine' dvd_trans _ hr
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
⊢ r = c 1 ^ ↑a * c 1 ^ (i - ↑a)
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
use c 1 ^ (i - (a : ℕ))
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
⊢ r = c 1 ^ i

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
⊢ ↑a ≤ i
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
⊢ r = c 1 ^ ↑a * c 1 ^ (i - ↑a)
rw [pow_mul_pow_sub (c 1)]
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
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)
apply Multiset.eq_replicate_of_mem
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
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
intro b hb
no goals
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
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)
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
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
have := UniqueFactorizationMonoid.normalizedFactors_prod (ne_zero_of_dvd_ne_zero hq hr)
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
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
rw [associated_iff_eq, hi, Multiset.prod_replicate] at this
no goals
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
rw [this]
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
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
conv_rhs => rw [← Finset.card_fin (i + 1)]
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

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
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
cases n
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
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
rw [Finset.card_image_iff]
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'
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
refine' Set.injOn_of_injective (fun m m' h => Fin.ext _) _
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
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'
refine'
  pow_injective_of_not_unit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) _ h
no goals
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
exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
no goals
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
contradiction
no goals
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
simp
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
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
simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
no goals
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
apply card_subset_divisors_le_length_of_chain (@h₂) H'
no goals
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
⊢ r = c 1 ^ i
exact H
no goals
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
⊢ ↑a ≤ i
exact Nat.succ_le_succ_iff.mp a.2