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
rw :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
    ringExpChar K ^ elemExponent K a
rw₁ : (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)).natDegree = ringExpChar K ^ elemExponent K a
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a
have rw₂ : ringExpChar K ^ elemExponent K a * natDegree.{u_2} (R := K) X = ringExpChar K ^ elemExponent K a
Tactic: rw [minpoly_eq K a, natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- 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
rw :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
    ringExpChar K ^ elemExponent K a
rw₁ : (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)).natDegree = ringExpChar K ^ elemExponent K a
rw₂ : ringExpChar K ^ elemExponent K a * natDegree.{u_2} (R := K) X = ringExpChar K ^ elemExponent K a
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a
have rw₃ : ringExpChar K ^ elemExponent K a * 1 = ringExpChar K ^ elemExponent K a
Tactic: rw [minpoly_eq K a, natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- 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
rw :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
    ringExpChar K ^ elemExponent K a
rw₁ : (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)).natDegree = ringExpChar K ^ elemExponent K a
rw₂ : ringExpChar K ^ elemExponent K a * natDegree.{u_2} (R := K) X = ringExpChar K ^ elemExponent K a
rw₃ : ringExpChar K ^ elemExponent K a * 1 = ringExpChar K ^ elemExponent K a
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a
have rw₄ : ringExpChar K ^ elemExponent K a = ringExpChar K ^ elemExponent K a
Tactic: rw [minpoly_eq K a, 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
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have this : Eq.{u_3 + 1} (α := L)
  ((aeval a : (a : K[X]) → L)
      (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
    L)
  (0 : L)
Tactic: have := minpoly_eq K a ▸ minpoly.aeval K 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 : IsPurelyInseparable K L
a : L
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa : ∀
  (this :
    HSub.hSub (α := L) (β := L)
        ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
        ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
      0),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa₁ : ∀
  (this :
    HSub.hSub (α := L) (β := L)
        ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
        ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
      0),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa₂ : ∀
  (this :
    HSub.hSub (β := L) (HPow.hPow (α := L) ((aeval a : (a : K[X]) → L) X : L) (ringExpChar K ^ elemExponent K a))
        ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
      0),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₂ :
  ∀
    (this :
      HSub.hSub (β := L) (HPow.hPow (α := L) ((aeval a : (a : K[X]) → L) X : L) (ringExpChar K ^ elemExponent K a))
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa₃ : ∀
  (this :
    HSub.hSub (β := L) (a ^ ringExpChar K ^ elemExponent K a) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
      0),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₂ :
  ∀
    (this :
      HSub.hSub (β := L) (HPow.hPow (α := L) ((aeval a : (a : K[X]) → L) X : L) (ringExpChar K ^ elemExponent K a))
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₃ :
  ∀
    (this :
      HSub.hSub (β := L) (a ^ ringExpChar K ^ elemExponent K a) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa₄ : ∀ (this : a ^ ringExpChar K ^ elemExponent K a = (algebraMap K L : (a : K) → L) (elemReduct K a)),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₂ :
  ∀
    (this :
      HSub.hSub (β := L) (HPow.hPow (α := L) ((aeval a : (a : K[X]) → L) X : L) (ringExpChar K ^ elemExponent K a))
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₃ :
  ∀
    (this :
      HSub.hSub (β := L) (a ^ ringExpChar K ^ elemExponent K a) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₄ :
  ∀ (this : a ^ ringExpChar K ^ elemExponent K a = (algebraMap K L : (a : K) → L) (elemReduct K a)),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
have rwa₅ : ∀ (this : (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a),
  (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Tactic: rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this
Cleared hypotheses: this
-- 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)
⊢ elemExponent K a ≤ n
have let : ∀ (p : ℕ), ExpChar K p → elemExponent K a ≤ n
Tactic: let ⟨p, _⟩ := ExpChar.exists K
-- 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
⊢ elemExponent K a ≤ n
have zero : ∀ [CharZero K], ExpChar K 1 → elemExponent K a ≤ n
Tactic: rcases ‹ExpChar K p› with _ | ⟨hp⟩
Cleared hypotheses: p, h_1
-- 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
zero : ∀ [CharZero K], ExpChar K 1 → elemExponent K a ≤ n
⊢ elemExponent K a ≤ n
have prime : ∀ (hp : Nat.Prime p) [CharP K p], elemExponent K a ≤ n
Tactic: rcases ‹ExpChar K p› with _ | ⟨hp⟩
-- 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
⊢ elemExponent K a ≤ n
have prime : ∀ (y : K) (hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n), elemExponent K a ≤ n
Tactic: obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h
-- 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])
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
have rwa : HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
    ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) y : K[X]) : L) =
  0
Tactic: rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- 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])
rwa :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) y : K[X]) : L) =
    0
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
have rwa₁ : HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
    ((algebraMap K L : (a : K) → L) y : L) =
  0
Tactic: rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- 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])
rwa :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) y : K[X]) : L) =
    0
rwa₁ :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((algebraMap K L : (a : K) → L) y : L) =
    0
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
have rwa₂ : HSub.hSub (β := L) (a ^ ringExpChar K ^ n) ((algebraMap K L : (a : K) → L) y : L) = 0
Tactic: rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- 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])
rwa :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) y : K[X]) : L) =
    0
rwa₁ :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((algebraMap K L : (a : K) → L) y : L) =
    0
rwa₂ : HSub.hSub (β := L) (a ^ ringExpChar K ^ n) ((algebraMap K L : (a : K) → L) y : L) = 0
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
have rwa₃ : a ^ ringExpChar K ^ n = (algebraMap K L : (a : K) → L) y
Tactic: rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- 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])
⊢ elemExponent K a ≤ n
have hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
Tactic: have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- 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)
⊢ elemExponent K a ≤ n
have hf₂ : f.Monic
Tactic: have hf₂ : f.Monic := monic_X_pow_sub_C y <| Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K _ _
-- 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
⊢ f.natDegree = ringExpChar K ^ n
have rw : (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)).natDegree = ringExpChar K ^ n
Tactic: rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- 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
⊢ f.natDegree = ringExpChar K ^ n
have rw₁ : ringExpChar K ^ n * natDegree.{u_2} (R := K) X = ringExpChar K ^ n
Tactic: rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- 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
⊢ f.natDegree = ringExpChar K ^ n
have rw₂ : ringExpChar K ^ n * 1 = ringExpChar K ^ n
Tactic: rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]