awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 0) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)
have a : p ^ n ≠ 0
Tactic: rw [(algebraMap K L).map_zero,
      algebraMap_iterateFrobeniusAux K p hn 0,
      zero_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (hypothesis)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b
have inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
Tactic: have inj := (algebraMap K L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (hypothesis)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b
have this : ExpChar L p
Tactic: have : ExpChar L p := expChar_of_injective_ringHom inj p
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b
have a₁ : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
  (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
Tactic: apply inj
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
have a₁ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
  HAdd.hAdd (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
    ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
Tactic: rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
have a₂ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
  HAdd.hAdd (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
Tactic: rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
have a₃ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) = a ^ p ^ n + b ^ p ^ n
Tactic: rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₃ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) = a ^ p ^ n + b ^ p ^ n
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
have a₄ : (a + b) ^ p ^ n = a ^ p ^ n + b ^ p ^ n
Tactic: rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) =
    HAdd.hAdd (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₃ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) = a ^ p ^ n + b ^ p ^ n
a₄ : (a + b) ^ p ^ n = a ^ p ^ n + b ^ p ^ n
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
have a₅ : a ^ p ^ n + b ^ p ^ n = a ^ p ^ n + b ^ p ^ n
Tactic: rw [(algebraMap K L).map_add,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a + b),
      add_pow_expChar_pow a b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : K
⊢ (iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) = a ^ p ^ n
have a₁ : Eq.{u_3 + 1} (α := L)
  (((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) : K) :
    L)
  (((algebraMap K L : K →+* L) : (a : K) → L) (a ^ p ^ n) : L)
Tactic: apply (algebraMap K L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : K
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (a ^ p ^ n) : L)
have a₁ : ((algebraMap K L : K →+* L) : (a : K) → L)
    ((iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) : K) =
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) (p ^ n)
Tactic: rw [map_pow, algebraMap_iterateFrobenius K p hn]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : K
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) : K) =
    HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) (p ^ n)
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (a ^ p ^ n) : L)
have a₂ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) a : L) (p ^ n) =
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) (p ^ n)
Tactic: rw [map_pow, algebraMap_iterateFrobenius K p hn]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ (↑(↑(iterateFrobenius K L p hn) : L →* K) : OneHom L K).toFun (r • a) =
    HSMul.hSMul (α := F) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F)
      ((↑(↑(iterateFrobenius K L p hn) : L →* K) : OneHom L K).toFun a)
have dsimp : iterateFrobeniusAux K L p n (r • a) =
  HSMul.hSMul (α := F) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) (iterateFrobeniusAux K L p n a)
Tactic: dsimp [iterateFrobenius]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ iterateFrobeniusAux K L p n (r • a) =
    HSMul.hSMul (α := F) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) (iterateFrobeniusAux K L p n a)
have rw : iterateFrobeniusAux K L p n (r • a) =
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
    (iterateFrobeniusAux K L p n a)
Tactic: rw [Algebra.smul_def _ (iterateFrobeniusAux K L p n a)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ iterateFrobeniusAux K L p n (r • a) =
    HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
      (iterateFrobeniusAux K L p n a)
have a₁ : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
  (((algebraMap K L : K →+* L) : (a : K) → L)
      (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
        (iterateFrobeniusAux K L p n a)) :
    L)
Tactic: apply (algebraMap K L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
          (iterateFrobeniusAux K L p n a)) :
      L)
have a₁ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
  HMul.hMul (α := L) (β := L)
    ((algebraMap K L : (a : K) → L)
        ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K) :
      L)
    ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
Tactic: rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K) :
        L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
          (iterateFrobeniusAux K L p n a)) :
      L)
have a₂ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
  HMul.hMul (α := L) (β := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
    ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
Tactic: rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K) :
        L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
          (iterateFrobeniusAux K L p n a)) :
      L)
have a₃ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
  HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
    (a ^ p ^ n)
Tactic: rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K) :
        L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
a₃ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      (a ^ p ^ n)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
          (iterateFrobeniusAux K L p n a)) :
      L)
have a₄ : (r • a) ^ p ^ n =
  HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
    (a ^ p ^ n)
Tactic: rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
inst_5 : Field F
inst_6 : Algebra F K
inst_7 : Algebra F L
inst_8 : IsScalarTower F K L
inst_9 : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K) :
        L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) (β := L)
      ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
a₃ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) =
    HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      (a ^ p ^ n)
a₄ :
  (r • a) ^ p ^ n =
    HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : L)
      (a ^ p ^ n)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (r • a)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        (HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) ((_root_.iterateFrobenius F p n : (a : F) → F) r : F) : K)
          (iterateFrobeniusAux K L p n a)) :
      L)
have a₅ : (r • a) ^ p ^ n = HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) (r ^ p ^ n) : L) (a ^ p ^ n)
Tactic: rw [(algebraMap K L).map_mul,
      ← IsScalarTower.algebraMap_apply,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn (r • a),
      iterateFrobenius_def,
      map_pow,
      Algebra.smul_def,
      mul_pow]