-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) : ∑ x : K, x ^ i = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
⊢ ∑ x : K, x ^ i = 0

Tactic:
by_cases hi : i = 0

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x : K, x ^ i = 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0

Tactic:
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
⊢ ∑ x : K, x ^ i = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i

Tactic:
exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0

Tactic:
classical
  have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
  let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩
  have : univ.map φ = univ \ {0} := by
    ext x
    simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
      mem_singleton, φ] using isUnit_iff_ne_zero
  calc
    ∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
      rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
    _ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
    _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x : K, x ^ i = 0

Tactic:
calc
  ∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
    rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
  _ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
  _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x : K, x ^ i = 0

Tactic:
simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
⊢ ∑ x : K, x ^ i = 0

Tactic:
let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
⊢ ∑ x : K, x ^ i = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
⊢ map φ univ = univ \ {0}

Tactic:
ext x

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
x : K
⊢ x ∈ map φ univ ↔ x ∈ univ \ {0}

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
x : K
⊢ x ∈ map φ univ ↔ x ∈ univ \ {0}

Tactic:
simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
  mem_singleton, φ] using isUnit_iff_ne_zero

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i

Tactic:
contrapose! h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x ∈ univ \ {0}, x ^ i = ∑ x : Kˣ, ↑x ^ i

Tactic:
simp [φ, ← this, univ.sum_map φ]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x : K, x ^ i = ∑ x ∈ univ \ {0}, x ^ i

Tactic:
rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
⊢ ∑ x : K, x ^ i = 0

Tactic:
have : univ.map φ = univ \ {0} := by
  ext x
  simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
    mem_singleton, φ] using isUnit_iff_ne_zero

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x : K, x ^ i = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x : Kˣ, ↑x ^ i = 0

Tactic:
rw [sum_pow_units K i, if_neg]

Result:
case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i

Proof state:
case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i

Tactic:
exact hiq

Result:
no goals