case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) (m + 1) } = φ (m + 1)
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) n } = φ n
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if coprime (ZMod.val a) (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if coprime (↑i) (m + 1) then 1 else 0
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // coprime (ZMod.val x) (m + 1) } = φ (m + 1)
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
  Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]
no goals
case intro
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a : ZMod (m + 1), if coprime (ZMod.val a) (m + 1) then 1 else 0) =
    ∑ i : Fin (m + 1), if coprime (↑i) (m + 1) then 1 else 0
rfl