case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ properDivisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range k)
n p : ℕ
pp : Prime p
k : ℕ
⊢ properDivisors (p ^ k) = map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range k)
ext a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ properDivisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range k)
simp only [mem_properDivisors, Nat.isUnit_iff, mem_map, mem_range, Function.Embedding.coeFn_mk,
  pow_eq]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ properDivisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
have := mem_properDivisors_prime_pow pp k (x := a)
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ properDivisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
rw [mem_properDivisors] at this
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ 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 ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : 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 ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
h : ∃ j x, a = p ^ j
⊢ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
rcases h with ⟨j, hj, hap⟩
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ j < k ∧ p ^ j = a
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
use j
no goals
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ j < k ∧ p ^ j = a
tauto
no goals
case a.refine_2
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ (∃ a_1, a_1 < k ∧ p ^ a_1 = a) → ∃ j x, a = p ^ j
tauto