case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ divisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range (k + 1))
n p : ℕ
pp : Prime p
k : ℕ
⊢ divisors (p ^ k) = map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range (k + 1))
ext a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ divisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range (k + 1))
simp only [mem_divisors, mem_map, mem_range, lt_succ_iff, Function.Embedding.coeFn_mk, Nat.pow_eq,
  mem_divisors_prime_pow pp k]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ divisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
have := mem_divisors_prime_pow pp k (x := a)
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ divisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
rw [mem_divisors] at this
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
rw [this]
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) → ∃ a_2, a_2 ≤ k ∧ p ^ a_2 = a

case a.refine_2
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a) → ∃ j x, a = p ^ j
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
refine ⟨?_, ?_⟩
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
h : ∃ j x, a = p ^ j
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) → ∃ a_2, a_2 ≤ k ∧ p ^ a_2 = a
intro h
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
h : ∃ j x, a = p ^ j
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
rcases h with ⟨x, hx, hap⟩
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ x ≤ k ∧ p ^ x = a
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
use x
no goals
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ x ≤ k ∧ p ^ x = a
tauto
no goals
case a.refine_2
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a) → ∃ j x, a = p ^ j
tauto