awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
this : Finset.card.{u_3} (α := L) univ ≤ (HPow.hPow (α := L[X]) X (q ^ m) - X).natDegree
refine_2 : max (HPow.hPow (α := L[X]) X (q ^ m)).natDegree (natDegree.{u_3} (R := L) X) = q ^ m
⊢ False

Tactic:
refine this.not_gt (((natDegree_sub_le ..).trans_eq ?_).trans_lt <|
      (Nat.pow_lt_pow_right Fintype.one_lt_card lt).trans_eq Module.card_eq_pow_finrank.symm)

Premises used: Fintype.one_lt_card, LE.le.trans_eq, Module.card_eq_pow_finrank, LT.lt.trans_eq, LE.le.not_gt, Eq.symm, LE.le.trans_lt, Polynomial.natDegree_sub_le, Nat.pow_lt_pow_right
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
this : Finset.card.{u_3} (α := L) univ ≤ (HPow.hPow (α := L[X]) X (q ^ m) - X).natDegree
⊢ max (HPow.hPow (α := L[X]) X (q ^ m)).natDegree (natDegree.{u_3} (R := L) X) = q ^ m

Tactic:
simp [Nat.one_le_pow _ _ Fintype.card_pos]

Premises used: Nat.one_le_pow, Fintype.card_pos
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
⊢ orderOf (G := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L

Tactic:
simpa [orderOf_eq_iff Module.finrank_pos, DFunLike.ext_iff] using orderOf_frobeniusAlgHom K L

Premises used: orderOf_eq_iff, DFunLike.ext_iff, FiniteField.orderOf_frobeniusAlgHom, Module.finrank_pos
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
e : Fin (Module.finrank K L) ≃ ↥(Submonoid.powers (frobeniusAlgHom K L)) :=
  Equiv.trans (Equiv.symm (finCongr ⋯)) (finEquivPowers ⋯)
⊢ Module.finrank K L = Nat.card (Fin (Module.finrank K L))

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
⊢ Function.Bijective (α := Fin (Module.finrank K L)) (β := L →ₐ[K] L)
    (Function.comp (β := Gal(L/K)) (⇑(Algebra.IsAlgebraic.algEquivEquivAlgHom K L) : (a : Gal(L/K)) → L →ₐ[K] L)
      fun (n : Fin (Module.finrank K L)) ↦ HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑n : ℕ))

Tactic:
simpa only [Function.comp_def, map_pow] using bijective_frobeniusAlgHom_pow K L

Premises used: map_pow, Function.comp_def, FiniteField.bijective_frobeniusAlgHom_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
x : L
⊢ Eq (α := L)
    ((((aeval (AlgHom.toLinearMap (frobeniusAlgHom K L)) : (a : K[X]) → L →ₗ[K] L)
              (HPow.hPow (α := K[X]) X (Module.finrank K L) - 1) :
            L →ₗ[K] L) :
          (a : L) → L)
        x :
      L)
    ((0 : (a : L) → L) x : L)

Tactic:
simpa [sub_eq_zero, Module.End.coe_pow, orderOf_frobeniusAlgHom] using
      congr($(pow_orderOf_eq_one (frobeniusAlgHom K L)) x)

Premises used: sub_eq_zero, Module.End.coe_pow, FiniteField.orderOf_frobeniusAlgHom
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
⊢ LinearIndependent.{0, u_1, u_3} K (M := L →ₗ[K] L) fun (i : Fin (Module.finrank K L)) ↦
    HPow.hPow (α := L →ₗ[K] L) (AlgHom.toLinearMap (frobeniusAlgHom K L)) (↑i : ℕ)

Tactic:
simpa [← AlgHom.toEnd_apply, ← map_pow] using (linearIndependent_algHom_toLinearMap K L L
        |>.restrict_scalars' K).comp _ (bijective_frobeniusAlgHom_pow K L).1

Premises used: linearIndependent_algHom_toLinearMap, map_pow, LinearIndependent.restrict_scalars', And.left, FiniteField.bijective_frobeniusAlgHom_pow, AlgHom.toEnd_apply, LinearIndependent.comp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
rw : LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)
⊢ degree.{u_3} (R := K') X < (HPow.hPow (α := K'[X]) X p).degree

Tactic:
rw [degree_X_pow, degree_X]

Premises used: Polynomial.degree_X_pow, Polynomial.degree_X
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
⊢ LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)

Tactic:
mod_cast hp

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
⊢ LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)

Tactic:
exact mod_cast hp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
⊢ degree.{u_3} (R := K') X < (HPow.hPow (α := K'[X]) X p).degree

Tactic:
have h1 : (X : K'[X]).degree < (X ^ p : K'[X]).degree := by
    rw [degree_X_pow, degree_X]
    exact mod_cast hp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
h1 : degree.{u_3} (R := K') X < (HPow.hPow (α := K'[X]) X p).degree
rw : (HPow.hPow (α := K'[X]) X p).natDegree = p
rw₁ rw₂ : p = p
⊢ (HPow.hPow (α := K'[X]) X p - X).natDegree = p

Tactic:
rw [natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), natDegree_X_pow]

Premises used: Polynomial.natDegree_X_pow, Polynomial.degree_sub_eq_left_of_degree_lt, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p n : ℕ
hn : n ≠ 0
hp : 1 < p
⊢ (HPow.hPow (α := K'[X]) X (p ^ n) - X).natDegree = p ^ n

Tactic:
X_pow_card_sub_X_natDegree_eq K' <| Nat.one_lt_pow hn hp

Premises used: Nat.one_lt_pow, FiniteField.X_pow_card_sub_X_natDegree_eq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p : ℕ
hp : 1 < p
⊢ HPow.hPow (α := K'[X]) X p - X ≠ 0

Tactic:
ne_zero_of_natDegree_gt <|
    calc
      1 < _ := hp
      _ = _ := (X_pow_card_sub_X_natDegree_eq K' hp).symm

Premises used: Trans.trans, Polynomial.ne_zero_of_natDegree_gt, FiniteField.X_pow_card_sub_X_natDegree_eq, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K' : Type u_3
inst : Field K'
p n : ℕ
hn : n ≠ 0
hp : 1 < p
⊢ HPow.hPow (α := K'[X]) X (p ^ n) - X ≠ 0

Tactic:
X_pow_card_sub_X_ne_zero K' <| Nat.one_lt_pow hn hp

Premises used: Nat.one_lt_pow, FiniteField.X_pow_card_sub_X_ne_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
⊢ HPow.hPow (α := K[X]) X q - X ≠ 0

Tactic:
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
rw : ∀ (x : K), x ∈ (HPow.hPow (α := K[X]) X q - X).roots.toFinset
⊢ (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ

Tactic:
rw [eq_univ_iff_forall]

Premises used: Finset.eq_univ_iff_forall
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
x : K
rw : x ∈ (HPow.hPow (α := K[X]) X q - X).roots
rw₁ : (HPow.hPow (α := K[X]) X q - X).IsRoot x
rw₂ : eval x (HPow.hPow (α := K[X]) X q - X) = 0
rw₃ : eval x (HPow.hPow (α := K[X]) X q) - eval x X = 0
rw₄ : eval x X ^ q - eval x X = 0
rw₅ : x ^ q - x = 0
rw₆ : x ^ q = x
rw₇ rw₈ : x = x
⊢ x ∈ (HPow.hPow (α := K[X]) X q - X).roots.toFinset

Tactic:
rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
        sub_eq_zero, pow_card]

Premises used: sub_eq_zero, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot.def, FiniteField.pow_card, Polynomial.mem_roots, Polynomial.eval_sub, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
⊢ (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ

Tactic:
have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ := by
      rw [eq_univ_iff_forall]
      intro x
      rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
        sub_eq_zero, pow_card]
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ
rw : (HPow.hPow (α := K[X]) X q - X).roots.Nodup
⊢ (HPow.hPow (α := K[X]) X q - X).roots = val univ

Tactic:
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]

Premises used: Multiset.dedup_eq_self, eq_comm, Multiset.toFinset_val
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ
hsep : (HPow.hPow (α := K[X]) X q - X).Separable
⊢ (HPow.hPow (α := K[X]) X q - X).roots.Nodup

Tactic:
apply nodup_roots

Premises used: Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ
⊢ IsCoprime (HPow.hPow (α := K[X]) X q - X) (-1)

Tactic:
isCoprime_one_right.neg_right (R := K[X])

Premises used: IsCoprime.neg_right, isCoprime_one_right
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ
h : Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X) : K[X]) (-1 : K[X])
⊢ IsCoprime (HPow.hPow (α := K[X]) X q - X) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X))

Tactic:
convert! isCoprime_one_right.neg_right (R := K[X]) using 1

Premises used: IsCoprime.neg_right, isCoprime_one_right
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
aux : HPow.hPow (α := K[X]) X q - X ≠ 0
this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ
h :
  HSub.hSub (α := K[X]) (β := K[X]) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q) : K[X])
      ((derivative : (a : K[X]) → K[X]) X : K[X]) =
    -1
h₁ :
  HSub.hSub (α := K[X]) (β := K[X]) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q) : K[X]) (1 : K[X]) =
    -1
h₂ : (C : (a : K) → K[X]) (↑q : K) * HPow.hPow (α := K[X]) X (q - 1) - 1 = -1
h₃ : (C : (a : K) → K[X]) 0 * HPow.hPow (α := K[X]) X (q - 1) - 1 = -1
h₄ : 0 * HPow.hPow (α := K[X]) X (q - 1) - 1 = -1
h₅ : HSub.hSub (α := K[X]) 0 1 = -1
h₆ h₇ : Eq.{u_1 + 1} (α := K[X]) (-1) (-1)
⊢ Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X) : K[X]) (-1 : K[X])

Tactic:
rw [derivative_sub, derivative_X, derivative_X_pow, Nat.cast_card_eq_zero K, C_0,
      zero_mul, zero_sub]

Premises used: Polynomial.derivative_X, Polynomial.C_0, MulZeroClass.zero_mul, Nat.cast_card_eq_zero, Polynomial.derivative_X_pow, Polynomial.derivative_sub, zero_sub
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
have have₁ have₂ : ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0), (HPow.hPow (α := K[X]) X q - X).roots = val univ
have₃ :
  ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0) (this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ),
    (HPow.hPow (α := K[X]) X q - X).roots = val univ
have₄ :
  ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0) (this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ),
    (HPow.hPow (α := K[X]) X q - X).roots.Nodup
hsep :
  ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0) (this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ),
    (HPow.hPow (α := K[X]) X q - X).Separable
hsep₁ :
  ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0) (this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ),
    IsCoprime (HPow.hPow (α := K[X]) X q - X) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X))
h :
  ∀ (aux : HPow.hPow (α := K[X]) X q - X ≠ 0) (this : (HPow.hPow (α := K[X]) X q - X).roots.toFinset = univ),
    Eq (α := K[X]) ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X q - X) : K[X]) (-1 : K[X])
⊢ (HPow.hPow (α := K[X]) X q - X).roots = val univ

Tactic:
classical
    have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
    have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ := by
      rw [eq_univ_iff_forall]
      intro x
      rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X,
        sub_eq_zero, pow_card]
    rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
    apply nodup_roots
    rw [separable_def]
    convert! isCoprime_one_right.neg_right (R := K[X]) using 1
    rw [derivative_sub, derivative_X, derivative_X_pow, Nat.cast_card_eq_zero K, C_0,
      zero_mul, zero_sub]

Premises used: IsCoprime.neg_right, Multiset.dedup_eq_self, Polynomial.derivative_X, Polynomial.C_0, MulZeroClass.zero_mul, Nat.cast_card_eq_zero, eq_comm, Polynomial.separable_def, isCoprime_one_right, Polynomial.derivative_X_pow, Polynomial.derivative_sub, Polynomial.nodup_roots, zero_sub, Multiset.toFinset_val
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
n : ℕ
hcard : q = p ^ n
a : ∀ (x : K), Eq (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) ((1 : (a : K) → K) x : K)
⊢ HPow.hPow (α := K →+* K) (frobenius K p) n = 1

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
rw : x ^ p ^ n
| (1 : (a : K) → K) x

Tactic:
rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]

Premises used: RingHom.id_apply, RingHom.one_def, FiniteField.pow_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
a : (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n
⊢ Eq (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) ((1 : (a : K) → K) x : K)

Tactic:
conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]

Premises used: RingHom.id_apply, RingHom.one_def, FiniteField.pow_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
x : K
⊢ (HPow.hPow (α := K →+* K) (β := ℕ) (frobenius K p) 0 : (a : K) → K) x = x ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
x : K
n : ℕ
hn : (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n
a : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ (n + 1)
a₁ : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ (p ^ n * p)
a₂ : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = (x ^ p ^ n) ^ p
a₃ : (RingHom.comp (frobenius K p) (HPow.hPow (α := K →+* K) (frobenius K p) n) : (a : K) → K) x = (x ^ p ^ n) ^ p
a₄ : (frobenius K p : (a : K) → K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) = (x ^ p ^ n) ^ p
a₅ : HPow.hPow (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) p = (x ^ p ^ n) ^ p
a₆ a₇ : (x ^ p ^ n) ^ p = (x ^ p ^ n) ^ p
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)

Tactic:
rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]

Premises used: RingHom.mul_def, pow_succ, pow_mul, frobenius_def, RingHom.comp_apply, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP K p
n : ℕ
x : K
a : (HPow.hPow (α := K →+* K) (β := ℕ) (frobenius K p) 0 : (a : K) → K) x = x ^ HPow.hPow (β := ℕ) p 0
a₁ :
  ∀ (n : ℕ) (hn : (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n),
    (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]

Premises used: RingHom.mul_def, pow_succ, pow_mul, frobenius_def, RingHom.comp_apply, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
obtain : ∀ (p : ℕ) (hp : CharP K p), (expand K q : (a : K[X]) → K[X]) f = f ^ q
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q

Tactic:
obtain ⟨p, hp⟩ := CharP.exists K

Premises used: CharP.exists
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
rcases :
  ∀ (n : ℕ) (npos : 0 < n) (hp : Nat.Prime p) (hn : q = p ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n npos) : ℕ)),
    (expand K q : (a : K[X]) → K[X]) f = f ^ q
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q

Tactic:
rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩

Premises used: FiniteField.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
p : ℕ
hp_1 : CharP K p
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n npos) : ℕ)
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
p : ℕ
hp_1 : CharP K p
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
rw : (expand K (p ^ n) : (a : K[X]) → K[X]) f = f ^ p ^ n
rw₁ :
  Eq (α := K[X]) ((expand K (p ^ n) : (a : K[X]) → K[X]) f : K[X])
    (Polynomial.map (iterateFrobenius K p n) ((expand K (p ^ n) : (a : K[X]) → K[X]) f) : K[X])
rw₂ :
  (expand K (p ^ n) : (a : K[X]) → K[X]) f =
    Polynomial.map (HPow.hPow (α := K →+* K) (frobenius K p) n) ((expand K (p ^ n) : (a : K[X]) → K[X]) f)
rw₃ :
  Eq (α := K[X]) ((expand K (p ^ n) : (a : K[X]) → K[X]) f : K[X])
    (Polynomial.map (R := K) 1 ((expand K (p ^ n) : (a : K[X]) → K[X]) f) : K[X])
rw₄ :
  Eq (α := K[X]) ((expand K (p ^ n) : (a : K[X]) → K[X]) f : K[X])
    (Polynomial.map (RingHom.id K) ((expand K (p ^ n) : (a : K[X]) → K[X]) f) : K[X])
rw₅ rw₆ :
  Eq (α := K[X]) ((expand K (p ^ n) : (a : K[X]) → K[X]) f : K[X]) ((expand K (p ^ n) : (a : K[X]) → K[X]) f : K[X])
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q

Tactic:
rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]

Premises used: RingHom.one_def, Polynomial.map_id, FiniteField.frobenius_pow, iterateFrobenius_eq_pow, Polynomial.map_iterateFrobenius_expand
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
inl :
  ∀ [hp : Fact (Nat.Prime 2)] (x : ZMod 2),
    ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
inr : ∀ (hp_odd : p % 2 = 1), ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
rcases hp.1.eq_two_or_odd with rfl | hp_odd

Premises used: Nat.Prime.eq_two_or_odd, rfl, Fact.out
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
x : ZMod 2
inl : ∀ (x : Fin 2), ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
change Fin 2 at x

Premises used: OfNat.ofNat, Fin
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
x : Fin 2
inl : ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩
inl₁ : ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
fin_cases x
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
h : ∃ (b : ZMod 2), HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩

Tactic:
use 0
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
⊢ ∃ (b : ZMod 2), HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
h : HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (α := ZMod 2) (β := ℕ) 1 2 = (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩

Tactic:
use 0, 1
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
hp : Fact (Nat.Prime 2)
⊢ HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (α := ZMod 2) (β := ℕ) 1 2 = (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
rw : p % 2 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Fintype.card (ZMod p) % 2 = 1

Tactic:
rw [ZMod.card, hp_odd]

Premises used: ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
inr :
  ∀ (a b : ZMod p) (hab : eval a f + eval b g = 0),
    ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
obtain ⟨a, b, hab⟩ : ∃ a b, f.eval a + g.eval b = 0 :=
    @exists_root_sum_quadratic _ _ _ _ f g (degree_X_pow 2) (degree_X_pow_sub_C (by decide) _)
      (by rw [ZMod.card, hp_odd])

Premises used: Polynomial.degree_X_pow_sub_C, Polynomial.degree_X_pow, FiniteField.exists_root_sum_quadratic, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
⟨a, b, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
a b : ZMod p
hab : eval a f + eval b g = 0
inr : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
refine ⟨a, b, ?_⟩