awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
intro :
  ∀ (n : σ → K),
    (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
        (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) n =
      e n
⊢ (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
    e

Tactic:
ext n
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
n : σ → K
intro : ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n
⊢ (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) n =
    e n

Tactic:
simp only [evalₗ_apply, map_sum, smul_eval]

Premises used: map_sum, MvPolynomial.smul_eval, MvPolynomial.evalₗ_apply
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
n : σ → K
intro : HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = e n
intro₁ :
  ∀ (b : σ → K),
    Membership.mem (γ := Finset (σ → K)) Finset.univ b →
      b ≠ n → HMul.hMul (β := K) (e b) ((eval n : (a : MvPolynomial σ K) → K) (indicator b) : K) = 0
intro₂ : n ∉ Finset.univ → HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = 0
⊢ ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n

Tactic:
rw [Finset.sum_eq_single n]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
n : σ → K
⊢ HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = e n

Tactic:
aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Premises used: MvPolynomial.eval_indicator_apply_eq_one, eq_comm, MvPolynomial.eval_indicator_apply_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
n : σ → K
⊢ ∀ (b : σ → K),
    Membership.mem (γ := Finset (σ → K)) Finset.univ b →
      b ≠ n → HMul.hMul (β := K) (e b) ((eval n : (a : MvPolynomial σ K) → K) (indicator b) : K) = 0

Tactic:
aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Premises used: MvPolynomial.eval_indicator_apply_eq_one, eq_comm, MvPolynomial.eval_indicator_apply_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
n : σ → K
⊢ n ∉ Finset.univ → HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = 0

Tactic:
aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Premises used: MvPolynomial.eval_indicator_apply_eq_one, eq_comm, MvPolynomial.eval_indicator_apply_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
e : (σ → K) → K
h : Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ e
intro :
  Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))
intro₁ intro₂ :
  (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
    e
⊢ ∃ (y : MvPolynomial σ K),
    Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) y ∧
      (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K) y = e

Tactic:
classical
  refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
  · exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)
  · ext n
    simp only [evalₗ_apply, map_sum, smul_eval]
    rw [Finset.sum_eq_single n] <;>
      aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Premises used: MvPolynomial.eval_indicator_apply_eq_one, HSub.hSub, MvPolynomial.restrictDegree, Fintype.card, MvPolynomial.indicator_mem_restrictDegree, map_sum, eq_comm, MvPolynomial.eval_indicator_apply_eq_zero, MvPolynomial.smul_eval, OfNat.ofNat, sum_mem, Submodule.smul_mem, MvPolynomial.evalₗ_apply
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
m : ℕ
simp : DecidablePred fun (n : σ →₀ ℕ) ↦ ∀ (i : σ), (n : (a : σ) → ℕ) i ≤ m
⊢ DecidablePred fun (x : σ →₀ ℕ) ↦
    Membership.mem (γ := Set (σ →₀ ℕ)) {n : σ →₀ ℕ | ∀ (i : σ), (n : (a : σ) → ℕ) i ≤ m} x

Tactic:
simp only [Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
m : ℕ
⊢ DecidablePred fun (n : σ →₀ ℕ) ↦ ∀ (i : σ), (n : (a : σ) → ℕ) i ≤ m

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
rw rw₁ :
  #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u) =
    #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u)
⊢ Module.rank K ((↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u) →₀ K) =
    #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u)

Tactic:
rw [rank_finsupp_self']

Premises used: rank_finsupp_self'
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
⊢ #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u) =
    #(↑{s : σ → ℕ | ∀ (n : σ), s n < Fintype.card K} : Type u)

Tactic:
Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩

Premises used: Cardinal, Cardinal.mk, Equiv.subtypeEquiv, Finsupp.equivFunOnFinite, Nonempty.intro, Quotient.mk', Quotient.sound
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
refine :
  ∀ (f : σ →₀ ℕ),
    Membership.mem (γ := Set (σ →₀ ℕ)) {s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} f ↔
      Membership.mem (α := σ → ℕ) (γ := Set (σ → ℕ)) {s : σ → ℕ | ∀ (n : σ), s n < Fintype.card K}
        ((Finsupp.equivFunOnFinite : (a : σ →₀ ℕ) → σ → ℕ) f : σ → ℕ)
⊢ #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u) =
    #(↑{s : σ → ℕ | ∀ (n : σ), s n < Fintype.card K} : Type u)

Tactic:
refine Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
f : σ →₀ ℕ
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) {s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} f ↔
    Membership.mem (α := σ → ℕ) (γ := Set (σ → ℕ)) {s : σ → ℕ | ∀ (n : σ), s n < Fintype.card K}
      ((Finsupp.equivFunOnFinite : (a : σ →₀ ℕ) → σ → ℕ) f : σ → ℕ)

Tactic:
forall_congr' fun n => le_tsub_iff_right ?_

Premises used: Set.Mem, setOf, forall_congr', le_tsub_iff_right
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
f : σ →₀ ℕ
refine : ∀ (n : σ), 1 ≤ Fintype.card K
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) {s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} f ↔
    Membership.mem (α := σ → ℕ) (γ := Set (σ → ℕ)) {s : σ → ℕ | ∀ (n : σ), s n < Fintype.card K}
      ((Finsupp.equivFunOnFinite : (a : σ →₀ ℕ) → σ → ℕ) f : σ → ℕ)

Tactic:
refine forall_congr' fun n => le_tsub_iff_right ?_

Premises used: forall_congr', le_tsub_iff_right
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
f : σ →₀ ℕ
n : σ
⊢ 1 ≤ Fintype.card K

Tactic:
Fintype.card_pos_iff.2 ⟨0⟩

Premises used: Iff.mpr, Nonempty.intro, OfNat.ofNat, Fintype.card_pos_iff, Nat.lt
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
f : σ →₀ ℕ
n : σ
⊢ 1 ≤ Fintype.card K

Tactic:
exact Fintype.card_pos_iff.2 ⟨0⟩

Premises used: Iff.mpr, Nonempty.intro, OfNat.ofNat, Fintype.card_pos_iff
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
intro : ∀ (val : Fintype σ), FiniteDimensional K (R σ K)
⊢ FiniteDimensional K (R σ K)

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
intro : Module.rank K (R σ K) < ℵ₀
⊢ FiniteDimensional K (R σ K)

Tactic:
rw [FiniteDimensional, ← IsNoetherian.iff_fg, IsNoetherian.iff_rank_lt_aleph0]

Premises used: IsNoetherian.iff_rank_lt_aleph0, IsNoetherian.iff_fg, FiniteDimensional
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ Module.rank K (R σ K) < ℵ₀

Tactic:
simpa only [rank_R] using Cardinal.natCast_lt_aleph0

Premises used: MvPolynomial.rank_R, Cardinal.natCast_lt_aleph0
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
⊢ Module.finrank K (R σ K) = Fintype.card.{u} (σ → K)

Tactic:
Module.finrank_eq_of_rank_eq (rank_R σ K)

Premises used: MvPolynomial.rank_R, Module.finrank_eq_of_rank_eq
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
rw : Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
⊢ Eq (α := Submodule K ((σ → K) → K)) (range (M := R σ K) (evalᵢ σ K)) ⊤

Tactic:
rw [evalᵢ, LinearMap.range_comp, range_subtype]

Premises used: LinearMap.range_comp, MvPolynomial.evalᵢ, Submodule.range_subtype
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤

Tactic:
map_restrict_dom_evalₗ K σ

Premises used: MvPolynomial.map_restrict_dom_evalₗ
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤

Tactic:
exact map_restrict_dom_evalₗ K σ

Premises used: MvPolynomial.map_restrict_dom_evalₗ
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
intro : ∀ (val : Fintype σ), Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥
⊢ Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥

Tactic:
(ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)

Premises used: Iff.mpr, LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank, MvPolynomial.range_evalᵢ
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
intro : Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
⊢ Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥

Tactic:
refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)

Premises used: Iff.mpr, LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank, MvPolynomial.range_evalᵢ
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
intro : Module.finrank K (R σ K) = Fintype.card.{u} (σ → K)
intro₁ intro₂ : Fintype.card.{u} (σ → K) = Fintype.card.{u} (σ → K)
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)

Tactic:
rw [Module.finrank_fintype_fun_eq_card, finrank_R]

Premises used: MvPolynomial.finrank_R, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
intro : Module.finrank K (R σ K) = Fintype.card.{u} (σ → K)
intro₁ intro₂ : Fintype.card.{u} (σ → K) = Fintype.card.{u} (σ → K)
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)

Tactic:
classical
  rw [Module.finrank_fintype_fun_eq_card, finrank_R]

Premises used: MvPolynomial.finrank_R, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.FieldTheory.Finite.Polynomial
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
p : MvPolynomial σ K
h : ∀ (v : σ → K), Eq (α := K) ((eval v : (a : MvPolynomial σ K) → K) p : K) (0 : K)
hp : Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) p
p' : R σ K :=
  Subtype.mk (p := fun (x : MvPolynomial σ K) ↦
    Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1)) x) p hp
this : Membership.mem (γ := Submodule K (R σ K)) (ker (evalᵢ σ K)) p'
rwa : ∀ (this : Membership.mem (γ := Submodule K (R σ K)) ⊥ p'), p' = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : p' = 0), p' = 0
⊢ p' = 0

Tactic:
rwa [ker_evalₗ, mem_bot] at this

Premises used: Submodule.mem_bot, MvPolynomial.ker_evalₗ
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ Fact (Nat.Prime (ringChar F))

Tactic:
haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ (∀ (y : F),
      Eq (α := ZMod (ringChar F))
        ((((Algebra.traceForm (ZMod (ringChar F)) F : (a : F) → F →ₗ[ZMod (ringChar F)] ZMod (ringChar F)) a :
                LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
              (a : F) → ZMod (ringChar F))
            y :
          ZMod (ringChar F))
        (0 : ZMod (ringChar F))) →
    a = 0

Tactic:
have htr := (traceForm_nondegenerate (ZMod (ringChar F)) F).1 a
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr :
  (∀ (y : F),
      Eq (α := ZMod (ringChar F))
        (((Algebra.trace (ZMod (ringChar F)) F :
                LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
              (a : F) → ZMod (ringChar F))
            (a * y) :
          ZMod (ringChar F))
        (0 : ZMod (ringChar F))) →
    a = 0
by_contra! :
  ∀
    (hf :
      ∀ (b : F),
        Eq (α := ZMod (ringChar F))
          (((Algebra.trace (ZMod (ringChar F)) F :
                  LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
                (a : F) → ZMod (ringChar F))
              (a * b) :
            ZMod (ringChar F))
          (0 : ZMod (ringChar F))),
    False
⊢ ∃ (b : F),
    Ne (α := ZMod (ringChar F))
      (((Algebra.trace (ZMod (ringChar F)) F :
              LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
            (a : F) → ZMod (ringChar F))
          (a * b) :
        ZMod (ringChar F))
      (0 : ZMod (ringChar F))

Tactic:
by_contra! hf
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr :
  (∀ (y : F),
      Eq (α := ZMod (ringChar F))
        (((Algebra.trace (ZMod (ringChar F)) F :
                LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
              (a : F) → ZMod (ringChar F))
            (a * y) :
          ZMod (ringChar F))
        (0 : ZMod (ringChar F))) →
    a = 0
hf :
  ∀ (b : F),
    Eq (α := ZMod (ringChar F))
      (((Algebra.trace (ZMod (ringChar F)) F :
              LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
            (a : F) → ZMod (ringChar F))
          (a * b) :
        ZMod (ringChar F))
      (0 : ZMod (ringChar F))
⊢ False

Tactic:
ha (htr hf)
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr :
  (∀ (y : F),
      Eq (α := ZMod (ringChar F))
        (((Algebra.trace (ZMod (ringChar F)) F :
                LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
              (a : F) → ZMod (ringChar F))
            (a * y) :
          ZMod (ringChar F))
        (0 : ZMod (ringChar F))) →
    a = 0
hf :
  ∀ (b : F),
    Eq (α := ZMod (ringChar F))
      (((Algebra.trace (ZMod (ringChar F)) F :
              LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
            (a : F) → ZMod (ringChar F))
          (a * b) :
        ZMod (ringChar F))
      (0 : ZMod (ringChar F))
⊢ False

Tactic:
exact ha (htr hf)
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
⊢ Finite K

Tactic:
have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this : Finite K
have :
  ∀ (this : Fintype K),
    Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K) : L)
      (∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K) : L)
    (∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)

Tactic:
have := ofFinite K
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this_1 : Finite K
this : Fintype K
rw :
  Eq.{u_2 + 1} (α := L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x)
    (∑ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K) : L)
    (∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)

Tactic:
rw [trace_eq_sum_automorphisms, Finset.sum_range]

Premises used: Finset.sum_range, trace_eq_sum_automorphisms
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this_1 : Finite K
this : Fintype K
i : Fin (Module.finrank K L)
rw : x ^ Nat.card K ^ (↑i : ℕ) = (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑i : ℕ)] x
rw₁ : x ^ Nat.card K ^ (↑i : ℕ) = (fun (x : L) ↦ x ^ Fintype.card K ^ (↑i : ℕ)) x
rw₂ rw₃ : x ^ Nat.card K ^ (↑i : ℕ) = (fun (x : L) ↦ x ^ Nat.card K ^ (↑i : ℕ)) x
⊢ x ^ Nat.card K ^ (↑i : ℕ) = (HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑i : ℕ) : (a : L) → L) x

Tactic:
rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

Premises used: AlgEquiv.coe_pow, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this_1 : Finite K
this : Fintype K
⊢ Eq.{u_2 + 1} (α := L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x)
    (∑ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))

Tactic:
exact Eq.symm <| sum_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <|
    fun i ↦ by rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

Premises used: Fintype.sum_bijective, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this : Finite K
have :
  ∀ (this : Fintype K),
    Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) x : K) : L)
      (∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) x : K) : L)
    (∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)

Tactic:
have := ofFinite K
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this_1 : Finite K
this : Fintype K
rw :
  Eq.{u_2 + 1} (α := L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x)
    (∏ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) x : K) : L)
    (∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i : L)

Tactic:
rw [Algebra.norm_eq_prod_automorphisms, Finset.prod_range]

Premises used: Algebra.norm_eq_prod_automorphisms, Finset.prod_range
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
this_1 : Finite K
this : Fintype K
⊢ Eq.{u_2 + 1} (α := L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x)
    (∏ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))

Tactic:
exact Eq.symm <| prod_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <|
    fun i ↦ by rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

Premises used: Fintype.prod_bijective, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Trace
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Finite L
inst_3 : Algebra K L
x : L
rw :
  ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i =
    HPow.hPow (β := ℕ) x (∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i)
rw₁ rw₂ :
  HPow.hPow (β := ℕ) x (∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i) =
    HPow.hPow (β := ℕ) x (∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i)
⊢ (algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) x : K) =
    HPow.hPow (β := ℕ) x (∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i)

Tactic:
rw [algebraMap_norm_eq_prod_pow, Finset.prod_pow_eq_pow_sum]

Premises used: FiniteField.algebraMap_norm_eq_prod_pow, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
ha : a ≠ 0
have :
  ∀ (this : Fintype Fq), Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
⊢ Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)

Tactic:
have : Fintype Fq := Fintype.ofFinite Fq