K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
let φ : Kˣ →* K :=
  { toFun := fun x => x ^ i
    map_one' := by simp
    map_mul' := by intros ; simp [mul_pow] }
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
have : Decidable (φ = 1) := by classical infer_instance
no goals
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
⊢ (fun x => ↑(x ^ i)) 1 = 1
simp
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
x✝ y✝ : Kˣ
⊢ OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } x✝ *
      OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } y✝
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
⊢ ∀ (x y : Kˣ),
    OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } x *
        OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } y
intros
no goals
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
x✝ y✝ : Kˣ
⊢ OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } x✝ *
      OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } y✝
simp [mul_pow]
no goals
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ Decidable (φ = 1)
classical infer_instance
no goals
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ Decidable (φ = 1)
infer_instance
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), ↑φ x = ↑1 x
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ q - 1 ∣ i ↔ φ = 1
rw [← forall_pow_eq_one_iff, FunLike.ext_iff]
case h
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ ↑φ a = ↑1 a
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), ↑φ x = ↑1 x
apply forall_congr'
case h
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ ↑φ x = ↑1 x
case h
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ ↑φ a = ↑1 a
intro x
no goals
case h
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ ↑φ x = ↑1 x
simp [Units.ext_iff]
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if
          { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
              map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
            1 then
        Fintype.card Kˣ
      else 0) =
    if
        { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
            map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
          1 then
      -1
    else 0
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0
simp only [this]
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1

case inr
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if
          { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
              map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
            1 then
        Fintype.card Kˣ
      else 0) =
    if
        { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
            map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
          1 then
      -1
    else 0
split_ifs
case inr
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0

case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1

case inr
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0
swap
no goals
case inr
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0
exact Nat.cast_zero
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1
rw [Fintype.card_units, Nat.cast_sub,
  cast_card_eq_zero, Nat.cast_one, zero_sub]
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
show 1 ≤ q
no goals
case inl
K : Type u_1
R : Type ?u.484011
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Fintype Kˣ
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
exact Fintype.card_pos_iff.mpr ⟨0⟩