-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem exists_chain_of_prime_pow {p : Associates M} {n : ℕ} (hn : n ≠ 0) (hp : Prime p) :
    ∃ c : Fin (n + 1) → Associates M,
      c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ i, r = c i

Proof state:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p

Tactic:
rw [Fin.val_one', Nat.mod_eq_of_lt, pow_one]

Result:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1

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

Tactic:
rintro ⟨i, rfl⟩

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

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

Tactic:
exact ⟨⟨i, Nat.lt_succ_of_le i_le⟩, hi⟩

Result:
no goals

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

Tactic:
rw [associated_iff_eq] at hi

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

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

Tactic:
dsimp only

Result:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p

Proof state:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1

Tactic:
exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)

Result:
no goals

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

Tactic:
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⟩

Result:
no goals

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

Tactic:
obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h

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

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

Tactic:
exact ⟨p ^ (n - i : ℕ), (pow_mul_pow_sub p (Nat.succ_le_succ_iff.mp i.2)).symm⟩

Result:
no goals

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

Tactic:
refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩

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

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

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

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