awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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
a₅ a₆ : a ^ p ^ n + 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)

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]

Premises used: Algebra.algebraMap, add_pow_expChar_pow, HAdd.hAdd, _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, RingHom.map_add
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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) ((iterateFrobenius K L p hn : (a : L) → K) a : K) = a ^ p ^ n

Tactic:
algebraMap_iterateFrobeniusAux K p hn a

Premises used: _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, _private.0.IsPurelyInseparable.iterateFrobeniusAux
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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₁ :
  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)
⊢ (iterateFrobenius K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) = a ^ p ^ n

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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)
a₂ 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)
⊢ 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:
rw [map_pow, algebraMap_iterateFrobenius K p hn]

Premises used: map_pow, IsPurelyInseparable.algebraMap_iterateFrobenius
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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
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)
⊢ (↑(↑(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)

Tactic:
dsimp [iterateFrobenius]

Premises used: IsPurelyInseparable.iterateFrobenius
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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
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)
⊢ 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:
rw [Algebra.smul_def _ (iterateFrobeniusAux K L p n a)]

Premises used: Algebra.smul_def, _private.0.IsPurelyInseparable.iterateFrobeniusAux
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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₁ :
  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)
⊢ 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:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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
a₈ 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
⊢ 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:
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]

Premises used: Algebra.algebraMap, map_pow, iterateFrobenius_def, _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, HSMul.hSMul, Algebra.smul_def, RingHom.map_mul, mul_pow, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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 : L
⊢ (algebraMap K L : (a : K) → L) ((iterateFrobeniusₛₗ F K L p hn : (a : L) → K) a : K) = a ^ p ^ n

Tactic:
algebraMap_iterateFrobenius K p hn a

Premises used: IsPurelyInseparable.algebraMap_iterateFrobenius, _private.0.IsPurelyInseparable.iterateFrobeniusAux
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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 : K
⊢ (iterateFrobeniusₛₗ F K L p hn : (a : L) → K) ((algebraMap K L : (a : K) → L) a : L) = a ^ p ^ n

Tactic:
iterateFrobenius_algebraMap L p hn a

Premises used: IsPurelyInseparable.iterateFrobenius_algebraMap, _private.0.IsPurelyInseparable.iterateFrobeniusAux
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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) (HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) a : K) (p ^ n)) : L)
⊢ (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)

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
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)
a₄ 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)
⊢ 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:
rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L p hn]

Premises used: map_pow, IsScalarTower.algebraMap_apply, IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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)
h : 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⁻¹

Tactic:
use n
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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)
h : 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)

Tactic:
rw [inv_pow]

Premises used: inv_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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)⁻¹

Tactic:
apply inv_mem (id hx : _ ∈ (⊥ : IntermediateField F E))

Premises used: id, InvMemClass.inv_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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 ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ ringExpChar F ^ n)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [mem_perfectClosure_iff, ringExpChar.eq F q]

Premises used: ringExpChar.eq, mem_perfectClosure_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
rw₁ 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)
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔ Polynomial.natSepDegree (minpoly F x) = 1

Tactic:
rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]

Premises used: ringExpChar, mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
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) ⊤
⊢ IsPurelyInseparable F E ↔ Eq (α := IntermediateField F E) (perfectClosure F E) ⊤

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]

Premises used: ringExpChar, isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ (∀ (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:
⟨fun H ↦ top_unique fun x _ ↦ H x, fun H _ ↦ H.ge trivial⟩

Premises used: Eq.ge, trivial, top_unique, Iff.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ (∀ (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:
exact ⟨fun H ↦ top_unique fun x _ ↦ H x, fun H _ ↦ H.ge trivial⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
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)
⊢ IsPurelyInseparable.{u, v} F ↥(perfectClosure F E)

Tactic:
rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]

Premises used: ringExpChar, isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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 : ↥(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:
fun ⟨_, n, y, h⟩ ↦ ⟨n, y, (algebraMap _ E).injective h⟩

Premises used: Algebra.algebraMap, perfectClosure, _private.0.perfectClosure.isPurelyInseparable.match_1, ringExpChar, Membership.mem, Exists, Subtype, RingHom.injective, HPow.hPow, RingHom.range, Exists.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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 : ↥(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:
exact fun ⟨_, n, y, h⟩ ↦ ⟨n, y, (algebraMap _ E).injective h⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
⊢ Algebra.IsAlgebraic.{u, v} F ↥(perfectClosure F E)

Tactic:
IsPurelyInseparable.isAlgebraic F _

Premises used: IsPurelyInseparable.isAlgebraic
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ Eq (α := IntermediateField F E) (perfectClosure F E) ⊥

Tactic:
haveI := Algebra.isSeparable_tower_bot_of_isSeparable F (perfectClosure F E) E
  eq_bot_of_isPurelyInseparable_of_isSeparable _

Premises used: perfectClosure, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
⊢ ∀ (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

Premises used: ringExpChar, isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
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
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x

Tactic:
obtain ⟨n, y, hy⟩ := h ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
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:
⟨n, y, congr_arg (algebraMap L E) hy⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Membership.mem, Subtype, congr_arg, Exists.intro, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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
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:
exact ⟨n, y, congr_arg (algebraMap L E) hy⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
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

Tactic:
⟨fun h ↦ (isPurelyInseparable_iff_pow_mem F (ringExpChar F)).2 fun x ↦ ?_,
    fun _ ↦ le_perfectClosure F E L⟩

Premises used: Iff.mpr, ringExpChar, isPurelyInseparable_iff_pow_mem, le_perfectClosure, Iff.intro