awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : CommSemiring K
a : K
p : MvPolynomial σ K
⊢ (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) (a • p)) =
    HSMul.hSMul (α := K) (β := (σ → K) → K) ((RingHom.id K : (a : K) → K) a : K) fun (e : σ → K) ↦
      (eval e : (a : MvPolynomial σ K) → K) p
have h : ∀ (e : σ → K),
  (eval e : (a : MvPolynomial σ K) → K) (a • p) =
    HSMul.hSMul (α := K) (β := (σ → K) → K) ((RingHom.id K : (a : K) → K) a : K)
      (fun (e : σ → K) ↦ (eval e : (a : MvPolynomial σ K) → K) p) e
Tactic: ext e
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
have intro : ∀ (val : Fintype σ),
  Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : Finite σ
val : Fintype σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
have intro : ∀ (e : (σ → K) → K),
  Membership.mem (γ := Submodule K ((σ → K) → K)) ⊤ 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: refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ ∃ (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
have intro : Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
  (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))
Tactic: refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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))
⊢ ∃ (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
have intro₁ : (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
  e
Tactic: refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
    e
have intro : ∀ (n : σ → K),
  (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) n =
    e n
Tactic: ext n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
      (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) n =
    e n
have intro : ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n
Tactic: simp only [evalₗ_apply, map_sum, smul_eval]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n
have intro : HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = e n
Tactic: rw [Finset.sum_eq_single n]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n
have 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
Tactic: rw [Finset.sum_eq_single n]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ ∑ x : σ → K, HMul.hMul (β := K) (e x) ((eval n : (a : MvPolynomial σ K) → K) (indicator x) : K) = e n
have intro₂ : n ∉ Finset.univ → HMul.hMul (β := K) (e n) ((eval n : (a : MvPolynomial σ K) → K) (indicator n) : K) = 0
Tactic: rw [Finset.sum_eq_single n]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ ∃ (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
have intro : Membership.mem (γ := Submodule K (MvPolynomial σ K)) (restrictDegree σ K (Fintype.card K - 1))
  (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n))
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])
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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))
⊢ ∃ (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
have intro₁ : (evalₗ K σ : (a : MvPolynomial σ K) → (σ → K) → K)
    (∑ n : σ → K, HSMul.hSMul (β := MvPolynomial σ K) (e n) (indicator n)) =
  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])
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
m : ℕ
⊢ DecidablePred fun (x : σ →₀ ℕ) ↦
    Membership.mem (γ := Set (σ →₀ ℕ)) {n : σ →₀ ℕ | ∀ (i : σ), (n : (a : σ) → ℕ) i ≤ m} x
have simp : DecidablePred fun (n : σ →₀ ℕ) ↦ ∀ (i : σ), (n : (a : σ) → ℕ) i ≤ m
Tactic: simp only [Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
⊢ 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)
have rw : #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u) =
  #(↑{s : σ →₀ ℕ | ∀ (n : σ), (s : (a : σ) → ℕ) n ≤ Fintype.card K - 1} : Type u)
Tactic: rw [rank_finsupp_self']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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)
have 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 : σ → ℕ)
Tactic: refine Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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 : σ → ℕ)
have refine : ∀ (n : σ), 1 ≤ Fintype.card K
Tactic: refine forall_congr' fun n => le_tsub_iff_right ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
⊢ FiniteDimensional K (R σ K)
have intro : ∀ (val : Fintype σ), FiniteDimensional K (R σ K)
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ FiniteDimensional K (R σ K)
have intro : Module.rank K (R σ K) < ℵ₀
Tactic: rw [FiniteDimensional, ← IsNoetherian.iff_fg, IsNoetherian.iff_rank_lt_aleph0]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
⊢ Eq (α := Submodule K ((σ → K) → K)) (range (M := R σ K) (evalᵢ σ K)) ⊤
have rw : Eq (α := Submodule K ((σ → K) → K)) (Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1))) ⊤
Tactic: rw [evalᵢ, LinearMap.range_comp, range_subtype]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
⊢ Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥
have intro : ∀ (val : Fintype σ), Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ Eq (α := Submodule K (R σ K)) (ker (evalᵢ σ K)) ⊥
have intro : Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
Tactic: refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
have intro : Module.finrank K (R σ K) = Fintype.card.{u} (σ → K)
Tactic: rw [Module.finrank_fintype_fun_eq_card, finrank_R]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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)
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
have intro₁ : Fintype.card.{u} (σ → K) = Fintype.card.{u} (σ → K)
Tactic: rw [Module.finrank_fintype_fun_eq_card, finrank_R]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ K : Type u
inst : Fintype K
inst_1 : Field K
inst_2 : Finite σ
val : Fintype σ
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
have intro : Module.finrank K (R σ K) = Fintype.card.{u} (σ → K)
Tactic: classical
  rw [Module.finrank_fintype_fun_eq_card, finrank_R]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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)
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)
have intro₁ : Fintype.card.{u} (σ → K) = Fintype.card.{u} (σ → K)
Tactic: classical
  rw [Module.finrank_fintype_fun_eq_card, finrank_R]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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'
⊢ p' = 0
have rwa : ∀ (this : Membership.mem (γ := Submodule K (R σ K)) ⊥ p'), p' = 0
Tactic: rwa [ker_evalₗ, mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
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
⊢ p' = 0
have rwa₁ : ∀ (this : p' = 0), p' = 0
Tactic: rwa [ker_evalₗ, mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
inst_2 : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ (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))
have this : Fact (Nat.Prime (ringChar F))
Tactic: haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (hypothesis)
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))
⊢ ∃ (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))
have htr : (∀ (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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ ∃ (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))
have 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
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (hypothesis)
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
⊢ 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)
have this : Finite K
Tactic: have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ 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)
have 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)
Tactic: have := ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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) ((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)
have rw : Eq.{u_2 + 1} (α := L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x) (∑ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))
Tactic: rw [trace_eq_sum_automorphisms, Finset.sum_range]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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)
⊢ x ^ Nat.card K ^ (↑i : ℕ) = (HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑i : ℕ) : (a : L) → L) x
have rw : x ^ Nat.card K ^ (↑i : ℕ) = (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[(↑i : ℕ)] x
Tactic: rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ x ^ Nat.card K ^ (↑i : ℕ) = (HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑i : ℕ) : (a : L) → L) x
have rw₁ : x ^ Nat.card K ^ (↑i : ℕ) = (fun (x : L) ↦ x ^ Fintype.card K ^ (↑i : ℕ)) x
Tactic: rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ x ^ Nat.card K ^ (↑i : ℕ) = (HPow.hPow (α := Gal(L/K)) (frobeniusAlgEquivOfAlgebraic K L) (↑i : ℕ) : (a : L) → L) x
have rw₂ : x ^ Nat.card K ^ (↑i : ℕ) = (fun (x : L) ↦ x ^ Nat.card K ^ (↑i : ℕ)) x
Tactic: rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (hypothesis)
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
⊢ 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)
have this : Finite K
Tactic: have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ 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)
have 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)
Tactic: have := ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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) ((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)
have rw : Eq.{u_2 + 1} (α := L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x) (∏ i : Fin (Module.finrank K L), x ^ Nat.card K ^ (↑i : ℕ))
Tactic: rw [Algebra.norm_eq_prod_automorphisms, Finset.prod_range]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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
⊢ (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)
have 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)
Tactic: rw [algebraMap_norm_eq_prod_pow, Finset.prod_pow_eq_pow_sum]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Trace (goal)
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)
⊢ (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)
have 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)
Tactic: rw [algebraMap_norm_eq_prod_pow, Finset.prod_pow_eq_pow_sum]