awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) x : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)
have rw : 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: rw [trace_eq_trace_adjoin K x, Algebra.smul_def, map_mul, ← adjoin.powerBasis_gen hx,
    trace_eq_sum_embeddings_gen E pb (IsAlgClosed.splits _), ← Algebra.smul_def,
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
rw :
  HSMul.hSMul (β := E) (finrank (↥K⟮x⟯) L) (∑ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) pb.gen) =
    ∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) x : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)
have rw₁ : IsSeparable K pb.gen
Tactic: rw [trace_eq_trace_adjoin K x, Algebra.smul_def, map_mul, ← adjoin.powerBasis_gen hx,
    trace_eq_sum_embeddings_gen E pb (IsAlgClosed.splits _), ← Algebra.smul_def,
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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
⊢ IsSeparable K pb.gen
have this : Algebra.IsSeparable.{u_4, u_5} K ↥K⟮x⟯
Tactic: haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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.{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)
have 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)
Tactic: apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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 L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∑ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure L)
have 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)
Tactic: rw [_root_.map_sum (algebraMap L (AlgebraicClosure L))]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
    (∑ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)
have 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)
Tactic: rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have a₁ : (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
Tactic: rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
    (∑ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
have 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)
Tactic: rw [← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq (α := L →ₗ[K] K) (trace K L) 0
have obtain : ∀ (p : ℕ) (hp : ExpChar K p), Eq (α := L →ₗ[K] K) (trace K L) 0
Tactic: obtain ⟨p, hp⟩ := ExpChar.exists K
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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
⊢ Eq (α := L →ₗ[K] K) (trace K L) 0
have this : p ≠ 0
Tactic: have := expChar_ne_zero K p
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq (α := L →ₗ[K] K) (trace K L) 0
have h : ∀ (x : L), Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have pos : ∀ (h₀ : FiniteDimensional K L), 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have neg : ∀ (h₀ : ¬FiniteDimensional K L), 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have neg : ¬∃ (s : Finset L), Nonempty (Basis (↥s) K L)
Tactic: rw [trace_eq_zero_of_not_exists_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have pos : ∀ (hx : IsSeparable K x), 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have neg : ∀ (hx : ¬IsSeparable K x), 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
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) x : K) ((0 : (a : L) → K) x : K)
have 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)
Tactic: lift x to separableClosure K L using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := K) ((trace K L : (a : L) → K) (↑x : L) : K) ((0 : (a : L) → K) (↑x : L) : K)
have 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)
Tactic: rw [← IntermediateField.algebraMap_apply, ← trace_trace (S := separableClosure K L),
      trace_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨n, hn⟩ := IsPurelyInseparable.finrank_eq_pow (separableClosure K L) L p
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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
⊢ 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)
have hn₁ : Algebra.IsSeparable K L
Tactic: rw [pow_zero, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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)
⊢ 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)
have hn₁ : Algebra.IsSeparable K L
Tactic: rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]