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
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)
a₅ : (r • a) ^ p ^ n = HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) (r ^ p ^ n) : 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 = HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * 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)
a₅ : (r • a) ^ p ^ n = HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) (r ^ p ^ n) : L) (a ^ p ^ n)
a₆ : (r • a) ^ p ^ n = HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * 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₇ : HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) r : L) a ^ p ^ n =
  HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * 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)
a₅ : (r • a) ^ p ^ n = HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) (r ^ p ^ n) : L) (a ^ p ^ n)
a₆ : (r • a) ^ p ^ n = HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * a ^ p ^ n
a₇ :
  HMul.hMul (α := L) ((algebraMap F L : (a : F) → L) r : L) a ^ p ^ n =
    HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * 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₈ : HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * a ^ p ^ n =
  HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) r : L) (p ^ n) * 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
a : F
⊢ (iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) =
    HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)
have a₁ : Eq.{u_3 + 1} (α := L)
  (((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
    L)
  (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : 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
a : F
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : L)
have a₁ : Eq.{u_3 + 1} (α := L)
  (((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
    L)
  (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap F K : (a : F) → K) (a ^ p ^ n) : K) : L)
Tactic: rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L 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
a : F
a₁ :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap F K : (a : F) → K) (a ^ p ^ n) : K) : L)
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : L)
have a₂ : Eq.{u_3 + 1} (α := L)
  (((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
    L)
  ((algebraMap F L : (a : F) → L) (a ^ p ^ n) : L)
Tactic: rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L 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
a : F
a₁ :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap F K : (a : F) → K) (a ^ p ^ n) : K) : L)
a₂ :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    ((algebraMap F L : (a : F) → L) (a ^ p ^ n) : L)
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : L)
have a₃ : ((algebraMap K L : K →+* L) : (a : K) → L)
    ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) =
  HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) a : L) (p ^ n)
Tactic: rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L 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
a : F
a₁ :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) ((algebraMap F K : (a : F) → K) (a ^ p ^ n) : K) : L)
a₂ :
  Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    ((algebraMap F L : (a : F) → L) (a ^ p ^ n) : L)
a₃ :
  ((algebraMap K L : K →+* L) : (a : K) → L)
      ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) =
    HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) a : L) (p ^ n)
⊢ Eq.{u_3 + 1} (α := L)
    (((algebraMap K L : K →+* L) : (a : K) → L)
        ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap F L : (a : F) → L) a : L) : K) :
      L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : L)
have a₄ : HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) a : L) (p ^ n) =
  HPow.hPow (α := L) ((algebraMap F L : (a : F) → L) a : L) (p ^ n)
Tactic: rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L p hn]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
x : E
n : ℕ
hx : Membership.mem (γ := Subsemiring E) (RingHom.rangeS (algebraMap F E)) (x ^ ringExpChar F ^ n)
⊢ Membership.mem (γ := Set E)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup
        (Subsemiring.toSubmonoid
          (Subalgebra.toSubsemiring.{u, v} (R := F)
            (have this : ExpChar E (ringExpChar F) := ⋯;
            Subalgebra.perfectClosure F E (ringExpChar F))))))
    x⁻¹
have h : Membership.mem (γ := Subsemiring E) (RingHom.rangeS (algebraMap F E)) (x⁻¹ ^ ringExpChar F ^ n)
Tactic: use n
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
x : E
n : ℕ
hx : Membership.mem (γ := Subsemiring E) (RingHom.rangeS (algebraMap F E)) (x ^ ringExpChar F ^ n)
⊢ Membership.mem (γ := Subsemiring E) (RingHom.rangeS (algebraMap F E)) (x⁻¹ ^ ringExpChar F ^ n)
have h : Membership.mem (γ := Subsemiring E) (RingHom.rangeS (algebraMap F E)) (x ^ ringExpChar F ^ n)⁻¹
Tactic: rw [inv_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
x : E
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have rw : (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
  ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
Tactic: rw [mem_perfectClosure_iff, ringExpChar.eq F q]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
x : E
rw :
  (∃ (n : ℕ),
      Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have rw₁ : (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)) ↔
  ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
Tactic: rw [mem_perfectClosure_iff, ringExpChar.eq F q]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔ Polynomial.natSepDegree (minpoly F x) = 1
have rw : (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
  Polynomial.natSepDegree (minpoly F x) = 1
Tactic: rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
rw :
  (∃ (n : ℕ),
      Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
    Polynomial.natSepDegree (minpoly F x) = 1
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔ Polynomial.natSepDegree (minpoly F x) = 1
have rw₁ : (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
  ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)
Tactic: rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsPurelyInseparable F E ↔ Eq (α := IntermediateField F E) (perfectClosure F E) ⊤
have rw : (∀ (x : E),
    ∃ (n : ℕ),
      Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) ↔
  Eq (α := IntermediateField F E) (perfectClosure F E) ⊤
Tactic: rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
⊢ IsPurelyInseparable.{u, v} F ↥(perfectClosure F E)
have rw : ∀ (x : ↥(perfectClosure F E)),
  ∃ (n : ℕ),
    Membership.mem (γ := Subring ↥(perfectClosure F E))
      (RingHom.range.{u, v} (R := F) (algebraMap F ↥(perfectClosure F E))) (x ^ ringExpChar F ^ n)
Tactic: rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable.{u, v} F ↥L
⊢ L ≤ perfectClosure F E
have h₁ : ∀ (x : ↥L),
  ∃ (n : ℕ), Membership.mem (γ := Subring ↥L) (RingHom.range.{u, v} (R := F) (algebraMap F ↥L)) (x ^ ringExpChar F ^ n)
Tactic: rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
h :
  ∀ (x : ↥L),
    ∃ (n : ℕ),
      Membership.mem (γ := Subring ↥L) (RingHom.range.{u, v} (R := F) (algebraMap F ↥L)) (x ^ ringExpChar F ^ n)
x : E
hx : x ∈ L
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
have obtain : ∀ (n : ℕ) (y : F)
  (hy :
    ((algebraMap F ↥L : RingHom.{u, v} F ↥L) : (a : F) → ↥L) y =
      Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx ^ ringExpChar F ^ n),
  Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
Tactic: obtain ⟨n, y, hy⟩ := h ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
⊢ L ≤ perfectClosure F E ↔ IsPurelyInseparable.{u, v} F ↥L
have refine : ∀ (h : L ≤ perfectClosure F E) (x : ↥L),
  ∃ (n : ℕ), Membership.mem (γ := Subring ↥L) (RingHom.range.{u, v} (R := F) (algebraMap F ↥L)) (x ^ ringExpChar F ^ n)
Tactic: refine ⟨fun h ↦ (isPurelyInseparable_iff_pow_mem F (ringExpChar F)).2 fun x ↦ ?_,
    fun _ ↦ le_perfectClosure F E L⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring ↥L) (RingHom.range.{u, v} (R := F) (algebraMap F ↥L)) (x ^ ringExpChar F ^ n)
have obtain : ∀ (n : ℕ) (y : F) (hy : (algebraMap F E : (a : F) → E) y = (↑x : E) ^ ringExpChar F ^ n),
  ∃ (n : ℕ), Membership.mem (γ := Subring ↥L) (RingHom.range.{u, v} (R := F) (algebraMap F ↥L)) (x ^ ringExpChar F ^ n)
Tactic: obtain ⟨n, y, hy⟩ := h x.2
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (perfectClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
have simp_rw : (∃ (n : ℕ),
    Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K))
      (HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n))) ↔
  ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)
Tactic: simp_rw [mem_perfectClosure_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ (∃ (n : ℕ),
      Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K))
        (HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n))) ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)
have refine_1 : (∃ (n : ℕ),
    Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K))
      (HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n))) →
  ∀ (n : ℕ) (y : F)
    (h :
      ((algebraMap F K : F →+* K) : (a : F) → K) y = HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n)),
    ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ ringExpChar F ^ n
Tactic: refine ⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
refine_1 :
  (∃ (n : ℕ),
      Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K))
        (HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n))) →
    ∀ (n : ℕ) (y : F)
      (h :
        ((algebraMap F K : F →+* K) : (a : F) → K) y =
          HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n)),
      ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ ringExpChar F ^ n
⊢ (∃ (n : ℕ),
      Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K))
        (HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n))) ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)
have refine_2 : (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)) →
  ∀ (n : ℕ) (y : F) (h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ ringExpChar F ^ n),
    ((algebraMap F K : F →+* K) : (a : F) → K) y = HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n)
Tactic: refine ⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩