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
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
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq
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
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
convert hi'
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
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
refine' (Nat.lt_succ_iff.1 i.prop).antisymm' (Nat.le_of_succ_le_succ _)
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
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
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 _
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
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
intro r hr
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
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
obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr
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
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
have := h₂.2 ⟨j, rfl⟩
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
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
rw [hi'] at this
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)
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
have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this
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)
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)
rcases h with ⟨u, hu, hu'⟩
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

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)
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)
refine' Finset.mem_image.mpr ⟨u, Finset.mem_univ _, _⟩
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
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
rw [associated_iff_eq] at hu'
no goals
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
rw [Fin.val_cast_of_lt (Nat.lt_succ_of_le hu), hu']
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)
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)
rw [← irreducible_iff_prime]
no goals
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)
exact second_of_chain_is_irreducible hn h₁ (@h₂) hq