awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
rw : (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)).natDegree = ringExpChar K ^ n
rw₁ : ringExpChar K ^ n * natDegree.{u_2} (R := K) X = ringExpChar K ^ n
rw₂ : ringExpChar K ^ n * 1 = ringExpChar K ^ n
⊢ f.natDegree = ringExpChar K ^ n
have rw₃ : ringExpChar K ^ n = ringExpChar K ^ n
Tactic: rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (hypothesis)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
⊢ elemExponent K a ≤ n
have hf₃ : f.natDegree = ringExpChar K ^ n
Tactic: have hf₃ : f.natDegree = ringExpChar K ^ n := by
      rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
⊢ HasExponent K L
have let : ∀ (p : ℕ), ExpChar K p → HasExponent K L
Tactic: let ⟨p, _⟩ := ExpChar.exists K
-- 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
⊢ HasExponent K L
have zero : ∀ [CharZero K], ExpChar K 1 → HasExponent K L
Tactic: rcases ‹ExpChar K p› with _ | ⟨hp⟩
Cleared hypotheses: p, h
-- 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
zero : ∀ [CharZero K], ExpChar K 1 → HasExponent K L
⊢ HasExponent K L
have prime : ∀ (hp : Nat.Prime p) [CharP K p], HasExponent K L
Tactic: rcases ‹ExpChar K p› with _ | ⟨hp⟩
-- 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
⊢ HasExponent K L
have prime : ∀ (a : L),
  ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
Tactic: refine ⟨e, fun a ↦ ⟨elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a), ?_⟩⟩
-- 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
Tactic: have h_elemexp_bound (a : L) : elemExponent K a ≤ e :=
      Nat.le_log_of_pow_le (Nat.Prime.one_lt <| ringExpChar.eq K p ▸ hp)
        (minpoly_natDegree_eq K a ▸ minpoly.natDegree_le 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have prime : HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
    (ringExpChar K ^ (e - elemExponent K a)) =
  a ^ ringExpChar K ^ e
Tactic: rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
prime :
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
      (ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have prime₁ : (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
Tactic: rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
prime :
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
      (ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
prime₁ : (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have prime₂ : a ^ (ringExpChar K ^ elemExponent K a * ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e
Tactic: rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
prime :
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
      (ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
prime₁ : (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
prime₂ : a ^ (ringExpChar K ^ elemExponent K a * ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have prime₃ : a ^ ringExpChar K ^ (elemExponent K a + (e - elemExponent K a)) = a ^ ringExpChar K ^ e
Tactic: rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound 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 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
prime :
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
      (ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
prime₁ : (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
prime₂ : a ^ (ringExpChar K ^ elemExponent K a * ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e
prime₃ : a ^ ringExpChar K ^ (elemExponent K a + (e - elemExponent K a)) = a ^ ringExpChar K ^ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
have prime₄ : a ^ ringExpChar K ^ e = a ^ ringExpChar K ^ e
Tactic: rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound a)]
-- 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 : L
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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 : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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 : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw₂ : (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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 : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₂ : (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw₃ : a ^ (p ^ elemExponent K a * p ^ (n - elemExponent K a)) = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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 : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₂ : (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n
rw₃ : a ^ (p ^ elemExponent K a * p ^ (n - elemExponent K a)) = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw₄ : a ^ p ^ (elemExponent K a + (n - elemExponent K a)) = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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 : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₂ : (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n
rw₃ : a ^ (p ^ elemExponent K a * p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₄ : a ^ p ^ (elemExponent K a + (n - elemExponent K a)) = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n
have rw₅ : a ^ p ^ n = a ^ p ^ n
Tactic: rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans 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
n : ℕ
hn : exponent K L ≤ n
⊢ iterateFrobeniusAux K L p n 1 = 1
have a : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
  (((algebraMap K L : K →+* L) : (a : K) → L) 1 : 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
n : ℕ
hn : exponent K L ≤ n
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 1 : L)
have a : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L) (1 : L)
Tactic: rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_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
n : ℕ
hn : exponent K L ≤ n
a : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L) (1 : L)
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 1 : L)
have a₁ : HPow.hPow (α := L) 1 (p ^ n) = 1
Tactic: rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_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
n : ℕ
hn : exponent K L ≤ n
a : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L) (1 : L)
a₁ : HPow.hPow (α := L) 1 (p ^ n) = 1
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 1 : L)
have a₂ : Eq.{u_3 + 1} (α := L) 1 1
Tactic: rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_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
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 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 (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
n : ℕ
hn : exponent K L ≤ n
a 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)) =
  HMul.hMul (α := 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_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      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
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (α := 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)) =
  HMul.hMul (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
Tactic: rw [(algebraMap K L).map_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      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
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (α := 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)) =
    HMul.hMul (β := 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_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      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
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (α := 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)) =
    HMul.hMul (β := 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_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      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
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (α := 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)) =
    HMul.hMul (β := 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_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      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
n : ℕ
hn : exponent K L ≤ n
⊢ iterateFrobeniusAux K L p n 0 = 0
have a : 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)
Tactic: apply (algebraMap K L).injective