-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_fixedPoints_modEq [DecidableEq α] {f : Function.End α} {p n : ℕ}
    [hp : Fact p.Prime] (hf : f ^ p ^ n = 1) :
    Fintype.card α ≡ Fintype.card f.fixedPoints [MOD p]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
  this ▸ (card_compl_support_modEq hσ).symm

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card ↑(fixedPoints f) = (support σ)ᶜ.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card ↑(fixedPoints f) = (support σ)ᶜ.card

Tactic:
suffices f.fixedPoints = (support σ)ᶜ by
  simp only [this]; apply Fintype.card_coe

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ fixedPoints f = ↑(support σ)ᶜ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
have hσ : σ ^ p ^ n = 1 := by
  rw [DFunLike.ext'_iff, coe_pow]
  exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ fixedPoints f = ↑(support σ)ᶜ

Tactic:
simp [σ, Set.ext_iff, IsFixedPt]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
  leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
  leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ (⇑σ)^[p ^ n] = ⇑1

Tactic:
exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ σ ^ p ^ n = 1

Tactic:
rw [DFunLike.ext'_iff, coe_pow]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ (⇑σ)^[p ^ n] = ⇑1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑↑(support σ)ᶜ = (support σ)ᶜ.card

Tactic:
apply Fintype.card_coe

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑(fixedPoints f) = (support σ)ᶜ.card

Tactic:
simp only [this]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑↑(support σ)ᶜ = (support σ)ᶜ.card