p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) =
    filter (fun x => ¬x ∈ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) = range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))
rw [sdiff_eq_filter]
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (p ^ (n + 1)) → (coprime (p ^ (n + 1)) x ↔ ¬x ∈ image (fun x => x * p) (range (p ^ n)))
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (coprime (p ^ (n + 1))) (range (p ^ (n + 1))) =
    filter (fun x => ¬x ∈ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))
apply filter_congr
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x < p ^ (n + 1) → (¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x))
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (p ^ (n + 1)) → (coprime (p ^ (n + 1)) x ↔ ¬x ∈ image (fun x => x * p) (range (p ^ n)))
simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
  hp.coprime_iff_not_dvd]
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (x : ℕ), x < p ^ (n + 1) → (¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x))
intro a ha
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

case H.mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
constructor
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
intro hap b h
case H.mp.intro
p : ℕ
hp : Prime p
n b : ℕ
left✝ : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
rcases h with ⟨_, rfl⟩
no goals
case H.mp.intro
p : ℕ
hp : Prime p
n b : ℕ
left✝ : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False
exact hap (dvd_mul_left _ _)
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
case H.mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
rintro h ⟨b, rfl⟩
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
rw [pow_succ'] at ha
no goals
case H.mpr.intro
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩
no goals
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
h2 : image (fun x => x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ Finset.card (range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)
rw [card_sdiff h2, card_image_of_injOn (h1.injOn _), card_range, card_range, ←
  one_mul (p ^ n), pow_succ', ← tsub_mul, one_mul, mul_comm]
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ a ∈ image (fun x => x * p) (range (p ^ n)) → a ∈ range (p ^ (n + 1))
simp only [mem_image, mem_range, exists_imp]
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
rintro b ⟨h, rfl⟩
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
rw [pow_succ]
no goals
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p
exact (mul_lt_mul_right hp.pos).2 h