-- Mathlib/NumberTheory/Divisors.lean
theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
    properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Tactic:
rw [mem_properDivisors] at this

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Proof state:
p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).properDivisors = map { toFun := fun x => p ^ x, inj' := ⋯ } (range k)

Tactic:
ext a

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range k)

Proof state:
case h.refine_2
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ a_1 < k, p ^ a_1 = a) → ∃ j, ∃ (_ : j < k), a = p ^ j

Tactic:
tauto

Result:
no goals

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ j, ∃ (_ : j < k), a = p ^ j) ↔ ∃ a_1 < k, p ^ a_1 = a

Tactic:
refine ⟨?_, ?_⟩

Result:
case h.refine_1
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ j, ∃ (_ : j < k), a = p ^ j) → ∃ a_2 < k, p ^ a_2 = a

case h.refine_2
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ a_1 < k, p ^ a_1 = a) → ∃ j, ∃ (_ : j < k), a = p ^ j

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Tactic:
have := mem_properDivisors_prime_pow pp k (x := a)

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Proof state:
case h.refine_1.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ ∃ a_1 < k, p ^ a_1 = a

Tactic:
use j

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ j < k ∧ p ^ j = a

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range k)

Tactic:
simp only [mem_properDivisors, Nat.isUnit_iff, mem_map, mem_range, Function.Embedding.coeFn_mk,
  pow_eq]

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Proof state:
case h.refine_1
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
h : ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ ∃ a_1 < k, p ^ a_1 = a

Tactic:
rcases h with ⟨j, hj, hap⟩

Result:
case h.refine_1.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ ∃ a_1 < k, p ^ a_1 = a

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Tactic:
rw [this]

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ j, ∃ (_ : j < k), a = p ^ j) ↔ ∃ a_1 < k, p ^ a_1 = a

Proof state:
case h.refine_1
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ (∃ j, ∃ (_ : j < k), a = p ^ j) → ∃ a_2 < k, p ^ a_2 = a

Tactic:
intro h

Result:
case h.refine_1
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
h : ∃ j, ∃ (_ : j < k), a = p ^ j
⊢ ∃ a_1 < k, p ^ a_1 = a

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ j < k ∧ p ^ j = a

Tactic:
tauto

Result:
no goals