awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
C :
  Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
⊢ Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
have C₁ : HPow.hPow (α := MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) p =
  (MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a
Tactic: rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
C :
  Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
C₁ :
  HPow.hPow (α := MvPolynomial σ (ZMod p))
      ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) p =
    (MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a
⊢ Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
have C₂ : Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
  ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) (a ^ p) : MvPolynomial σ (ZMod p))
  ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
Tactic: rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
C :
  Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
C₁ :
  HPow.hPow (α := MvPolynomial σ (ZMod p))
      ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) p =
    (MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a
C₂ :
  Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) (a ^ p) : MvPolynomial σ (ZMod p))
    ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
⊢ Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
have C₃ : Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
  ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
  ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
Tactic: rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
      Eq (α := MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
            MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p)) →
        Eq (α := MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) :
            MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) : MvPolynomial σ (ZMod p))
have add : ∀ (p_1 q : MvPolynomial σ (ZMod p)),
  Eq (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
    Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p)) →
      HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
            MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
            MvPolynomial σ (ZMod p)) =
        HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 q : MvPolynomial σ (ZMod p)
hf :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
hg :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
⊢ HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
        MvPolynomial σ (ZMod p)) =
    HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
have add : HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
      MvPolynomial σ (ZMod p)) =
  HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 q : MvPolynomial σ (ZMod p)
hf :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
hg :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
add :
  HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
        MvPolynomial σ (ZMod p)) =
    HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
⊢ HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
        MvPolynomial σ (ZMod p)) =
    HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
have add₁ : HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p)) =
  HAdd.hAdd (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p))
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
      Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 * X n) :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 * X n) : MvPolynomial σ (ZMod p))
have mul_X : ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
  Eq (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
    HMul.hMul (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
          MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (X n) :
          MvPolynomial σ (ZMod p)) =
      HMul.hMul (α := MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
        (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
Tactic: simp only [expand_X, map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 : MvPolynomial σ (ZMod p)
n : σ
hf :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
⊢ HMul.hMul (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (X n) :
        MvPolynomial σ (ZMod p)) =
    HMul.hMul (α := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
have mul_X : HMul.hMul (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (X n) :
      MvPolynomial σ (ZMod p)) =
  HMul.hMul (α := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
Tactic: rw [hf, frobenius_def]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 : MvPolynomial σ (ZMod p)
n : σ
hf :
  Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
mul_X :
  HMul.hMul (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (X n) :
        MvPolynomial σ (ZMod p)) =
    HMul.hMul (α := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
⊢ HMul.hMul (α := MvPolynomial σ (ZMod p)) (β := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (X n) :
        MvPolynomial σ (ZMod p)) =
    HMul.hMul (α := MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
      (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
have mul_X₁ : HMul.hMul (α := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p) =
  HMul.hMul (α := MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p))
    (HPow.hPow (α := MvPolynomial σ (ZMod p)) (X n) p)
Tactic: rw [hf, frobenius_def]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (hypothesis)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
a : σ → K
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator a) : K) (1 : K)
have a₁ : Nontrivial K
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (hypothesis)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
a : σ → K
h : Nontrivial K
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator a) : K) (1 : K)
have this : 0 < Fintype.card K - 1
Tactic: have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine : ∀ (s : σ),
  Membership.mem (γ := Finset σ) Finset.univ s →
    degrees.{u_1, u_2} (R := K) 1 ∪
        (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
              ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
            (Fintype.card K - 1)).degrees ≤
      HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
Tactic: refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ degrees.{u_1, u_2} (R := K) 1 ∪
      (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
            ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
          (Fintype.card K - 1)).degrees ≤
    HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
have rw : (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
        ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
      (Fintype.card K - 1)).degrees ≤
  HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
Tactic: rw [degrees_one, Multiset.zero_union]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
          ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
        (Fintype.card K - 1)).degrees ≤
    HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
have refine : (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
      ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
  {s}
Tactic: refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
        ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K)).degrees ≤
    {s}
have refine : degrees.{u_1, u_2} (R := K) (X s) ∪ degrees.{u_1, u_2} (R := K) ((C : (a : K) → MvPolynomial σ K) (c s)) ≤ {s}
Tactic: refine degrees_sub_le.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
s : σ
h : Membership.mem (γ := Finset σ) Finset.univ s
⊢ degrees.{u_1, u_2} (R := K) (X s) ∪ degrees.{u_1, u_2} (R := K) ((C : (a : K) → MvPolynomial σ K) (c s)) ≤ {s}
have rw : degrees.{u_1, u_2} (R := K) (X s) ≤ {s}
Tactic: rw [degrees_C, Multiset.union_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine : ∀ (s : σ),
  Membership.mem (γ := Finset σ) Finset.univ s →
    degrees.{u_1, u_2} (R := K) 1 ∪
        (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
              ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
            (Fintype.card K - 1)).degrees ≤
      HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
Tactic: classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
c : σ → K
refine :
  ∀ (s : σ),
    Membership.mem (γ := Finset σ) Finset.univ s →
      degrees.{u_1, u_2} (R := K) 1 ∪
          (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
                ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
              (Fintype.card K - 1)).degrees ≤
        HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
⊢ LE.le.{u_2} (α := Multiset σ)
    (degrees.{u_1, u_2} (R := K)
      (∏ n : σ,
        (1 -
          HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X n)
              ((C : (a : K) → MvPolynomial σ K) (c n) : MvPolynomial σ K) ^
            (Fintype.card K - 1))))
    (∑ s : σ, HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s})
have refine₁ : ∀ (s : σ),
  Membership.mem (γ := Finset σ) Finset.univ s →
    (HSub.hSub (α := MvPolynomial σ K) (β := MvPolynomial σ K) (X s)
            ((C : (a : K) → MvPolynomial σ K) (c s) : MvPolynomial σ K) ^
          (Fintype.card K - 1)).degrees ≤
      HSMul.hSMul (β := Multiset σ) (Fintype.card K - 1) {s}
Tactic: classical
  refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
  rw [degrees_one, Multiset.zero_union]
  refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
  refine degrees_sub_le.trans ?_
  rw [degrees_C, Multiset.union_zero]
  exact degrees_X' _