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
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
refine' ⟨fun i => p ^ (i : ℕ), _, fun n m h => _, @fun y => ⟨fun h => _, _⟩⟩
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p
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
dsimp only
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ p ^ ↑1 = p
rw [Fin.val_one', Nat.mod_eq_of_lt, pow_one]
no goals
case refine'_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ 1 < n + 1
exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)
no goals
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
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⟩
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
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
obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h
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
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
rw [associated_iff_eq] at hi
no goals
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
exact ⟨⟨i, Nat.lt_succ_of_le i_le⟩, hi⟩
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
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
rintro ⟨i, rfl⟩
no goals
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
exact ⟨p ^ (n - i : ℕ), (pow_mul_pow_sub p (Nat.succ_le_succ_iff.mp i.2)).symm⟩