-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sum_pow_units [DecidableEq K] (i : ℕ) :
    (∑ x : Kˣ, (x ^ i : K)) = if q - 1 ∣ i then -1 else 0

Proof state:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ φ x = 1 x

Tactic:
simp [φ, Units.ext_iff]

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

Tactic:
swap

Result:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∀ (x y : Kˣ),
    { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun (x * y) =
      { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun x * { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun y

Tactic:
intros

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
x✝ y✝ : Kˣ
⊢ { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun (x✝ * y✝) =
    { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun x✝ * { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun y✝

Proof state:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ 1 ≤ q

Tactic:
exact Fintype.card_pos_iff.mpr ⟨0⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ ∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Tactic:
have : Decidable (φ = 1) := by classical infer_instance

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ ∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ Decidable (φ = 1)

Tactic:
infer_instance

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
x✝ y✝ : Kˣ
⊢ { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun (x✝ * y✝) =
    { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun x✝ * { toFun := fun x => ↑x ^ i, map_one' := ⋯ }.toFun y✝

Tactic:
simp [mul_pow]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0

Tactic:
simp only [this]

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if φ = 1 then -1 else 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if φ = 1 then -1 else 0

Tactic:
split_ifs

Result:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

Proof state:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

Tactic:
rw [Fintype.card_units, Nat.cast_sub,
  cast_card_eq_zero, Nat.cast_one, zero_sub]

Result:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ 1 ≤ q

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Tactic:
let φ : Kˣ →* K :=
  { toFun := fun x => x ^ i
    map_one' := by simp
    map_mul' := by intros; simp [mul_pow] }

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ ∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ Decidable (φ = 1)

Tactic:
classical infer_instance

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ φ a = 1 a

Tactic:
intro x

Result:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ φ x = 1 x

Proof state:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

Tactic:
exact Nat.cast_zero

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), φ x = 1 x

Tactic:
apply forall_congr'

Result:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ φ a = 1 a

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ (fun x => ↑x ^ i) 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ q - 1 ∣ i ↔ φ = 1

Tactic:
rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), φ x = 1 x