-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem eq_pow_second_of_chain_of_has_chain {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

Proof state:
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

Tactic:
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq

Result:
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

Proof state:
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, Associated (c j) (c 1 ^ i_1)
⊢ c j ∈ Finset.image (fun m => c 1 ^ ↑m) Finset.univ

Tactic:
rcases h with ⟨u, hu, hu'⟩

Result:
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

Proof state:
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

Tactic:
rw [Fin.val_cast_of_lt (Nat.lt_succ_of_le hu), hu']

Result:
no goals

Proof state:
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

Tactic:
have := h₂.2 ⟨j, rfl⟩

Result:
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

Proof state:
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

Tactic:
rw [associated_iff_eq] at hu'

Result:
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

Proof state:
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

Tactic:
have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this

Result:
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, 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)