awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
⊢ Finite K

Tactic:
have := Finite.of_injective _ (algebraMap K L).injective
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
this : Finite K
rw : Nat.card.{u_4} Gal(K/F) = Module.finrank F K
rw₁ rw₂ : Module.finrank F K = Module.finrank F K
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
rw [Nat.card_congr (Normal.algHomEquivAut F L K), IsGalois.card_aut_eq_finrank]

Premises used: Normal.algHomEquivAut, IsGalois.card_aut_eq_finrank, Nat.card_congr
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
inst_6 : Finite K
h : Module.finrank F K ∣ Module.finrank F L
rw : Nat.card (K →ₐ[F] L) = Module.finrank F K
rw₁ rw₂ : Module.finrank F K = Module.finrank F K
⊢ Fintype.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
rw [Fintype.card_eq_nat_card, natCard_algHom_of_finrank_dvd h]

Premises used: FiniteField.natCard_algHom_of_finrank_dvd, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
⊢ Nonempty (K →ₐ[F] L) ↔ Module.finrank F K ∣ Module.finrank F L

Tactic:
⟨fun ⟨f⟩ ↦ ?_, nonempty_algHom_of_finrank_dvd⟩

Premises used: FiniteField.nonempty_algHom_of_finrank_dvd, Dvd.dvd, _private.0.FiniteField.nonempty_algHom_iff_finrank_dvd.match_1, Iff.intro, Module.finrank
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
refine : Nonempty (K →ₐ[F] L) → ∀ (f : K →ₐ[F] L), Module.finrank F K ∣ Module.finrank F L
⊢ Nonempty (K →ₐ[F] L) ↔ Module.finrank F K ∣ Module.finrank F L

Tactic:
refine ⟨fun ⟨f⟩ ↦ ?_, nonempty_algHom_of_finrank_dvd⟩
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
rw : Module.finrank F K ∣ Module.finrank F K * Module.finrank K L
⊢ Module.finrank F K ∣ Module.finrank F L

Tactic:
rw [← Module.finrank_mul_finrank F K L]

Premises used: Module.finrank_mul_finrank
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
⊢ Module.finrank F K ∣ Module.finrank F K * Module.finrank K L

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
⊢ Module.finrank F K ∣ Module.finrank F K * Module.finrank K L

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
n : ℕ
φ : MvPolynomial σ ℤ
⊢ (C : (a : ℤ) → MvPolynomial σ ℤ) (↑n : ℤ) ∣ φ ↔
    Eq (α := MvPolynomial σ (ZMod n))
      ((map (Int.castRingHom (ZMod n)) : (a : MvPolynomial σ ℤ) → MvPolynomial σ (ZMod n)) φ : MvPolynomial σ (ZMod n))
      (0 : MvPolynomial σ (ZMod n))

Tactic:
C_dvd_iff_map_hom_eq_zero _ _ (CharP.intCast_eq_zero_iff (ZMod n) n) _

Premises used: MvPolynomial.C_dvd_iff_map_hom_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
C :
  ∀ (a : 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))
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)) →
        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))
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)) →
      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))
⊢ Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f : MvPolynomial σ (ZMod p))

Tactic:
apply induction_on f

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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))
C₃ 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))
⊢ 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))

Tactic:
rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]

Premises used: MvPolynomial.expand_C, ZMod.pow_card, frobenius_def, MvPolynomial.C_pow
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
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))
⊢ ∀ (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))

Tactic:
simp only [map_add]

Premises used: map_add
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 : MvPolynomial σ (ZMod p)
add :
  ∀ (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))
⊢ ∀ (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:
_
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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))
add₁ 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))
⊢ 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:
rw [hf, hg]
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
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)
⊢ ∀ (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))

Tactic:
simp only [expand_X, map_mul]

Premises used: MvPolynomial.expand_X, map_mul
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f p_1 : MvPolynomial σ (ZMod p)
mul_X :
  ∀ (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)
⊢ ∀ (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:
_
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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)
mul_X₁ 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)
⊢ 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:
rw [hf, frobenius_def]

Premises used: frobenius_def
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ (expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f = f ^ p

Tactic:
(frobenius_zmod _).symm

Premises used: MvPolynomial.frobenius_zmod, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
a : σ → K
⊢ Nontrivial K

Tactic:
nontriviality
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
a : σ → K
h : Nontrivial K
⊢ 0 < Fintype.card K - 1

Tactic:
have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Fintype σ
inst_2 : CommRing K
a : σ → K
h : Nontrivial K
this : 0 < Fintype.card K - 1
⊢ Eq.{u_1 + 1} (α := K) ((eval a : (a : MvPolynomial σ K) → K) (indicator a) : K) (1 : K)

Tactic:
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
    zero_pow this.ne', sub_zero, Finset.prod_const_one]

Premises used: map_sub, sub_self, sub_zero, map_pow, map_prod, LT.lt.ne', Finset.prod_const_one, map_one, MvPolynomial.eval_C, MvPolynomial.eval_X, zero_pow, MvPolynomial.indicator
-- Module: Mathlib.FieldTheory.Finite.Polynomial
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})

Tactic:
degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_

Premises used: MvPolynomial.degrees_sub_le, MvPolynomial.degrees_prod_le, Finset.sum_le_sum, LE.le.trans