-- Mathlib/Data/Nat/Totient.lean
theorem totient_prime_pow_succ {p : ℕ} (hp : p.Prime) (n : ℕ) : φ (p ^ (n + 1)) = p ^ n * (p - 1) :=
  calc
    φ (p ^ (n + 1)) = #{a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} :=
      totient_eq_card_coprime _
    _ = #(range (p ^ (n + 1)) \ (range (p ^ n)).image (· * p)) :=
      congr_arg card
        (by
          rw [sdiff_eq_filter]
          apply filter_congr
          simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]
          intro a ha
          constructor
          · intro hap b h; rcases h with ⟨_, rfl⟩
            exact hap (dvd_mul_left _ _)
          · rintro h ⟨b, rfl⟩
            rw [pow_succ'] at ha
            exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩)
    _ = _

Proof state:
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)

Tactic:
intro a ha

Result:
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Proof state:
case H.mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
intro hap b h

Result:
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

Proof state:
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun x => x * p) (range (p ^ n))

Tactic:
simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
  hp.coprime_iff_not_dvd]

Result:
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)

Proof state:
case H
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
constructor

Result:
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

Proof state:
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))
⊢ #(range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))) = p ^ n * (p - 1)

Tactic:
rw [card_sdiff h2, Finset.card_image_of_injective _ h1, card_range, card_range, ←
  one_mul (p ^ n), pow_succ', ← tsub_mul, one_mul, mul_comm]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (fun a => (p ^ (n + 1)).Coprime a) (range (p ^ (n + 1))) =
    filter (fun x => x ∉ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))

Tactic:
apply filter_congr

Result:
case H
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun x => x * p) (range (p ^ n))

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (fun a => (p ^ (n + 1)).Coprime a) (range (p ^ (n + 1))) =
    range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))

Tactic:
rw [sdiff_eq_filter]

Result:
p : ℕ
hp : Prime p
n : ℕ
⊢ filter (fun a => (p ^ (n + 1)).Coprime a) (range (p ^ (n + 1))) =
    filter (fun x => x ∉ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))

Proof state:
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Tactic:
exact (mul_lt_mul_right hp.pos).2 h

Result:
no goals

Proof state:
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

Tactic:
rcases h with ⟨_, rfl⟩

Result:
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

Proof state:
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

Tactic:
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)

Tactic:
rintro b ⟨h, rfl⟩

Result:
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)

Proof state:
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)

Tactic:
rw [Nat.pow_succ]

Result:
case intro
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Proof state:
case H.mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a

Tactic:
rintro h ⟨b, rfl⟩

Result:
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

Proof state:
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

Tactic:
rw [pow_succ'] at ha

Result:
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

Proof state:
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

Tactic:
exact hap (dvd_mul_left _ _)

Result:
no goals

Proof state:
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))

Tactic:
simp only [mem_image, mem_range, exists_imp]

Result:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x => x * p
a : ℕ
⊢ ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)