awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ HSMul.hSMul (β := E) (finrank (↥K⟮x⟯) L) (∑ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) pb.gen) =
    ∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x

Tactic:
exact (sum_embeddings_eq_finrank_mul L E pb).symm

Premises used: sum_embeddings_eq_finrank_mul, Eq.symm
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ Algebra.IsSeparable.{u_4, u_5} K ↥K⟮x⟯

Tactic:
haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
this : Algebra.IsSeparable.{u_4, u_5} K ↥K⟮x⟯
⊢ IsSeparable K pb.gen

Tactic:
Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
this : Algebra.IsSeparable.{u_4, u_5} K ↥K⟮x⟯
⊢ IsSeparable K pb.gen

Tactic:
exact Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure L)
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K) : L)
    (∑ σ : Gal(L/K), (σ : (a : L) → L) x : L)

Tactic:
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)

Premises used: FaithfulSMul.algebraMap_injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∑ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure L)

Tactic:
rw [_root_.map_sum (algebraMap L (AlgebraicClosure L))]

Premises used: Algebra.algebraMap, map_sum, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∑ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
a₁ : (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
a₂ :
  ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    Eq (α := AlgebraicClosure L) ((x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
      ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
          ((((Normal.algHomEquivAut K (AlgebraicClosure L) L : (a : L →ₐ[K] AlgebraicClosure L) → Gal(L/K)) x_1 :
                Gal(L/K)) :
              (a : L) → L)
            x) :
        AlgebraicClosure L)
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∑ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)

Tactic:
rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]

Premises used: Normal.algHomEquivAut, Fintype.sum_equiv, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((Algebra.trace K L : (a : L) → K) x) :
      AlgebraicClosure L)
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∑ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)

Tactic:
rw [← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)]

Premises used: trace_eq_sum_embeddings, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((Algebra.trace K L : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((Algebra.trace K L : (a : L) → K) x) :
      AlgebraicClosure L)

Tactic:
simp only [algebraMap_eq_smul_one, smul_one_smul]

Premises used: Algebra.algebraMap_eq_smul_one, smul_one_smul
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
σ : L →ₐ[K] AlgebraicClosure L
⊢ Eq (α := AlgebraicClosure L) ((σ : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((((Normal.algHomEquivAut K (AlgebraicClosure L) L : (a : L →ₐ[K] AlgebraicClosure L) → Gal(L/K)) σ :
              Gal(L/K)) :
            (a : L) → L)
          x) :
      AlgebraicClosure L)

Tactic:
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
      AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]

Premises used: Normal.algHomEquivAut, RingHom.id_apply, Algebra.algebraMap_self, AlgEquiv.coe_ofBijective, Equiv.coe_fn_mk, AlgHom.restrictNormal', AlgHom.restrictNormal_commutes
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
obtain : ∀ (p : ℕ) (hp : ExpChar K p), Eq (α := L →ₗ[K] K) (trace K L) 0
⊢ Eq (α := L →ₗ[K] K) (trace K L) 0

Tactic:
obtain ⟨p, hp⟩ := ExpChar.exists K

Premises used: ExpChar.exists
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
⊢ p ≠ 0

Tactic:
have := expChar_ne_zero K p
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h : ∀ (x : L), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
⊢ Eq (α := L →ₗ[K] K) (trace K L) 0

Tactic:
ext x
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
pos : ∀ (h₀ : FiniteDimensional K L), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
neg : ∀ (h₀ : ¬FiniteDimensional K L), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)

Tactic:
by_cases h₀ : FiniteDimensional K L

Premises used: FiniteDimensional
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
neg : ¬∃ (s : Finset L), Nonempty (Basis (↥s) K L)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)

Tactic:
rw [trace_eq_zero_of_not_exists_basis]

Premises used: Algebra.trace_eq_zero_of_not_exists_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
s : Finset L
b : Basis (↥s) K L
⊢ False

Tactic:
h₀ (Module.Finite.of_basis b)

Premises used: Module.Finite.of_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
s : Finset L
b : Basis (↥s) K L
⊢ False

Tactic:
exact h₀ (Module.Finite.of_basis b)

Premises used: Module.Finite.of_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
pos : ∀ (hx : IsSeparable K x), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
neg : ∀ (hx : ¬IsSeparable K x), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)

Tactic:
by_cases hx : IsSeparable K x

Premises used: IsSeparable
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : IsSeparable K x
⊢ Membership.mem (γ := IntermediateField K L) (separableClosure K L) x

Tactic:
hx

Premises used: Set.Mem, setOf, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : IsSeparable K x
pos :
  ∀ (x : ↥(separableClosure K L)),
    Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) (↑x : L) : K) ((0 : (a : L) → K) (↑x : L) : K)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)

Tactic:
lift x to separableClosure K L using hx

Premises used: separableClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
pos :
  Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) (↑x : L) : K) ((0 : (a : L) → K) (↑x : L) : K)

Tactic:
rw [← IntermediateField.algebraMap_apply, ← trace_trace (S := separableClosure K L),
      trace_algebraMap]

Premises used: Algebra.trace_algebraMap, IntermediateField.algebraMap_apply, Algebra.trace_trace
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
pos :
  ∀ (n : ℕ) (hn : finrank (↥(separableClosure K L)) L = p ^ n),
    Eq.{u_4 + 1} (α := K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
        K)
      ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
obtain ⟨n, hn⟩ := IsPurelyInseparable.finrank_eq_pow (separableClosure K L) L p

Premises used: IsPurelyInseparable.finrank_eq_pow, Membership.mem, Subtype, separableClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
hn : finrank (↥(separableClosure K L)) L = HPow.hPow (β := ℕ) p 0
⊢ Algebra.IsSeparable K L

Tactic:
rw [pow_zero, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn

Premises used: separableClosure.eq_top_iff, IntermediateField.finrank_eq_one_iff_eq_top, pow_zero
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
hn : Algebra.IsSeparable K L
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
cases H hn
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst_3 : CharZero K
this : Ne (α := ℕ) 1 0
hn : finrank (↥(separableClosure K L)) L = HPow.hPow (α := ℕ) 1 (n + 1)
⊢ Algebra.IsSeparable K L

Tactic:
rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn

Premises used: one_pow, separableClosure.eq_top_iff, IntermediateField.finrank_eq_one_iff_eq_top
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst_3 : CharZero K
this : Ne (α := ℕ) 1 0
hn : Algebra.IsSeparable K L
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
cases H hn
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar : CharP K p
pos :
  Eq.{u_4 + 1} (α := K) ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (p ^ (n + 1) • x) : K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₁ :
  Eq.{u_4 + 1} (α := K) ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) ((p * p ^ n) • x) : K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₂ :
  Eq.{u_4 + 1} (α := K) ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (p • p ^ n • x) : K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₃ :
  HSMul.hSMul (β := K) p ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (p ^ n • x) : K) =
    (0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L)
pos₄ :
  HMul.hMul (α := K) (β := K) ((↑p : K) : K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (p ^ n • x) : K) =
    (0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L)
pos₅ :
  HMul.hMul (α := K) (β := K) (0 : K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (p ^ n • x) : K) =
    (0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L)
pos₆ :
  Eq.{u_4 + 1} (α := K) (0 : K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₇ pos₈ : Eq.{u_4 + 1} (α := K) 0 0
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]

Premises used: CharP.cast_eq_zero, LinearMap.zero_apply, MulZeroClass.zero_mul, nsmul_eq_mul, LinearMap.map_smul_of_tower, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
pos :
  ∀ [CharZero K] (this : Ne (α := ℕ) 1 0) (hn : finrank (↥(separableClosure K L)) L = HPow.hPow (α := ℕ) 1 (n + 1)),
    Eq.{u_4 + 1} (α := K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
        K)
      ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₁ :
  ∀ (hprime : Nat.Prime p) [CharP K p],
    Eq.{u_4 + 1} (α := K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
        K)
      ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
cases hp with
      | zero =>
        rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
        cases H hn
      | prime hprime =>
        rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]

Premises used: CharP.cast_eq_zero, one_pow, LinearMap.zero_apply, MulZeroClass.zero_mul, separableClosure.eq_top_iff, IntermediateField.finrank_eq_one_iff_eq_top, nsmul_eq_mul, LinearMap.map_smul_of_tower, Matrix.zero, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ n
pos :
  ∀ (hn : finrank (↥(separableClosure K L)) L = HPow.hPow (β := ℕ) p 0),
    Eq.{u_4 + 1} (α := K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
        K)
      ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
pos₁ :
  ∀ (n : ℕ) (hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)),
    Eq.{u_4 + 1} (α := K)
      ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
        K)
      ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K ↥(separableClosure K L) : (a : ↥(separableClosure K L)) → K) (finrank (↥(separableClosure K L)) L • x) :
      K)
    ((0 : (a : L) → K) ((algebraMap (↥(separableClosure K L)) L : (a : ↥(separableClosure K L)) → L) x : L) : K)

Tactic:
cases n with
    | zero =>
      rw [pow_zero, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
      cases H hn
    | succ n =>
      cases hp with
      | zero =>
        rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
        cases H hn
      | prime hprime =>
        rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]

Premises used: CharP.cast_eq_zero, one_pow, LinearMap.zero_apply, MulZeroClass.zero_mul, separableClosure.eq_top_iff, IntermediateField.finrank_eq_one_iff_eq_top, pow_zero, nsmul_eq_mul, LinearMap.map_smul_of_tower, Matrix.zero, SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
neg : (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)

Tactic:
rw [trace_eq_finrank_mul_minpoly_nextCoeff]

Premises used: trace_eq_finrank_mul_minpoly_nextCoeff
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
neg :
  ∀ (g : K[X]) (hg₁ : g.Separable) (m : ℕ)
    (hg₂ : Eq (α := K[X]) ((expand K (p ^ m) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])),
    (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
⊢ (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x

Tactic:
obtain ⟨g, hg₁, m, hg₂⟩ :=
      (minpoly.irreducible (IsIntegral.isIntegral (R := K) x)).hasSeparableContraction p

Premises used: Algebra.IsIntegral.isIntegral, Irreducible.hasSeparableContraction, minpoly.irreducible