awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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))
⊢ (HPow.hPow (α := K[X]) X q - X).roots = val univ
have 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])
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ HPow.hPow (α := K →+* K) (frobenius K p) n = 1
have a : ∀ (x : K), Eq (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) ((1 : (a : K) → K) x : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
| (1 : (a : K) → K) x
have rw : x ^ p ^ n
Tactic: rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) ((1 : (a : K) → K) x : K)
have a : (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n
Tactic: conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₁ : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ (p ^ n * p)
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₂ : (frobenius K p * HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = (x ^ p ^ n) ^ p
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₃ : (RingHom.comp (frobenius K p) (HPow.hPow (α := K →+* K) (frobenius K p) n) : (a : K) → K) x = (x ^ p ^ n) ^ p
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₄ : (frobenius K p : (a : K) → K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) = (x ^ p ^ n) ^ p
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₅ : HPow.hPow (α := K) ((HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x : K) p = (x ^ p ^ n) ^ p
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) (n + 1) : (a : K) → K) x = x ^ p ^ (n + 1)
have a₆ : (x ^ p ^ n) ^ p = (x ^ p ^ n) ^ p
Tactic: rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n
have a : (HPow.hPow (α := K →+* K) (β := ℕ) (frobenius K p) 0 : (a : K) → K) x = x ^ HPow.hPow (β := ℕ) p 0
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := K →+* K) (frobenius K p) n : (a : K) → K) x = x ^ p ^ n
have 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)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have obtain : ∀ (p : ℕ) (hp : CharP K p), (expand K q : (a : K[X]) → K[X]) f = f ^ q
Tactic: obtain ⟨p, hp⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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
Tactic: rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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) : ℕ)
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have rw : (expand K (p ^ n) : (a : K[X]) → K[X]) f = f ^ p ^ n
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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])
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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])
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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)
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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])
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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])
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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])
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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])
⊢ (expand K q : (a : K[X]) → K[X]) f = f ^ q
have 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])
Tactic: rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inl : ∀ [hp : Fact (Nat.Prime 2)] (x : ZMod 2),
  ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
Tactic: rcases hp.1.eq_two_or_odd with rfl | hp_odd
Cleared hypotheses: p, hp, x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ ∃ (a : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inr : ∀ (hp_odd : p % 2 = 1), ∃ (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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inl : ∀ (x : Fin 2), ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
Tactic: change Fin 2 at x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inl : ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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, ⋯⟩
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inl₁ : ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
hp : Fact (Nat.Prime 2)
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩
have h : ∃ (b : ZMod 2), HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩
Tactic: use 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
hp : Fact (Nat.Prime 2)
⊢ ∃ (a : ZMod 2) (b : ZMod 2), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩
have h : HPow.hPow (α := ZMod 2) (β := ℕ) 0 2 + HPow.hPow (α := ZMod 2) (β := ℕ) 1 2 = (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩
Tactic: use 0, 1
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Fintype.card (ZMod p) % 2 = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [ZMod.card, hp_odd]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ZMod p) (b : ZMod p), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have 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
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])
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have inr : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
Tactic: refine ⟨a, b, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x
have inr : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - x = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
⊢ ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]
have rcases : ∀ (a b : ZMod p) (hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)),
  ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]
Tactic: rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]
have refine : HPow.hPow (α := ℤ) (β := ℕ) (↑a.valMinAbs.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b.valMinAbs.natAbs : ℤ) 2 ≡
  x [ZMOD (↑p : ℤ)]
Tactic: refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _,
    ZMod.natAbs_valMinAbs_le _, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a.valMinAbs.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b.valMinAbs.natAbs : ℤ) 2 ≡
    x [ZMOD (↑p : ℤ)]
have hx₁ : HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
    HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
  (↑x : ZMod p)
Tactic: rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a.valMinAbs.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b.valMinAbs.natAbs : ℤ) 2 ≡
    x [ZMOD (↑p : ℤ)]
have push_cast : HPow.hPow (β := ℕ) |a.valMinAbs| 2 + HPow.hPow (β := ℕ) |b.valMinAbs| 2 ≡ x [ZMOD (↑p : ℤ)]
Tactic: push_cast
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
⊢ HPow.hPow (β := ℕ) |a.valMinAbs| 2 + HPow.hPow (β := ℕ) |b.valMinAbs| 2 ≡ x [ZMOD (↑p : ℤ)]
have rw : Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) a.valMinAbs 2 + HPow.hPow (β := ℕ) b.valMinAbs 2) : ZMod p) (↑x : ZMod p)
Tactic: rw [sq_abs, sq_abs, ← ZMod.intCast_eq_intCast_iff]