awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ L ≤ perfectClosure F E ↔ IsPurelyInseparable.{u, v} F ↥L

Tactic:
refine ⟨fun h ↦ (isPurelyInseparable_iff_pow_mem F (ringExpChar F)).2 fun x ↦ ?_,
    fun _ ↦ le_perfectClosure F E L⟩
-- 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 : L ≤ perfectClosure F E
x : ↥L
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)
⊢ ∃ (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

Premises used: Subtype.property
-- 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 : L ≤ perfectClosure F E
x : ↥L
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:
⟨n, y, (algebraMap L E).injective hy⟩

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, 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
L : IntermediateField F E
h : L ≤ perfectClosure F E
x : ↥L
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:
exact ⟨n, y, (algebraMap L E).injective 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
⊢ Eq (α := IntermediateField F E) (separableClosure F E ⊓ perfectClosure F E) ⊥

Tactic:
haveI := (le_separableClosure_iff F E _).mp (inf_le_left (b := perfectClosure F E))
  haveI := (le_perfectClosure_iff F E _).mp (inf_le_right (a := separableClosure F E))
  eq_bot_of_isPurelyInseparable_of_isSeparable _

Premises used: perfectClosure, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable, separableClosure, Min.min
-- 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
i : E →ₐ[F] K
x : E
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)
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (perfectClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x

Tactic:
simp_rw [mem_perfectClosure_iff]

Premises used: 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
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)

Tactic:
⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩

Premises used: Algebra.algebraMap, ringExpChar, Membership.mem, Exists, _private.0.map_mem_perfectClosure_iff.match_1, HPow.hPow, RingHom.range, Iff.intro, Exists.intro, DFunLike.coe, _private.0.map_mem_perfectClosure_iff.match_2
-- 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
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
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)
⊢ (∃ (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:
refine ⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩
-- 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
i : E →ₐ[F] K
x : E
h_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)
⊢ Function.Injective.{v + 1, w + 1} (α := E) (β := K) (⇑i : (a : E) → K)

Tactic:
i.injective

Premises used: RingHom.injective, AlgHom.toRingHom
-- 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
i : E →ₐ[F] K
x : E
h_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)
refine_1 :
  Eq.{w + 1} (α := K) ((i : (a : E) → K) (((algebraMap F E : F →+* E) : (a : F) → E) y : E) : K)
    ((i : (a : E) → K) (x ^ ringExpChar F ^ n) : K)
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ ringExpChar F ^ n

Tactic:
apply_fun i using i.injective

Premises used: RingHom.injective, AlgHom.toRingHom
-- 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
i : E →ₐ[F] K
x : E
h_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)
refine_1 : Eq.{w + 1} (α := K) ((algebraMap F K : (a : F) → K) y : K) ((i : (a : E) → K) (x ^ ringExpChar F ^ n) : K)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  (algebraMap F K : (a : F) → K) y = HPow.hPow (α := K) ((i : (a : E) → K) x : K) (ringExpChar F ^ n)
⊢ Eq.{w + 1} (α := K) ((i : (a : E) → K) (((algebraMap F E : F →+* E) : (a : F) → E) y : E) : K)
    ((i : (a : E) → K) (x ^ ringExpChar F ^ n) : K)

Tactic:
rwa [AlgHom.commutes, map_pow]

Premises used: map_pow, AlgHom.commutes
-- 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
i : E →ₐ[F] K
x : E
h_1 :
  ∃ (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:
simpa only [AlgHom.commutes, map_pow] using congr_arg i h

Premises used: map_pow, congr_arg, AlgHom.commutes, 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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
h : ∀ (x : E), x ∈ comap i (perfectClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
⊢ comap i (perfectClosure F K) = perfectClosure F E

Tactic:
ext x
-- 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
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (perfectClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x

Tactic:
map_mem_perfectClosure_iff i

Premises used: Set.Mem, setOf, map_mem_perfectClosure_iff, Set.preimage
-- 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
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (perfectClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x

Tactic:
exact map_mem_perfectClosure_iff i

Premises used: map_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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
⊢ map i (perfectClosure F E) ≤ perfectClosure F K

Tactic:
map_le_iff_le_comap.mpr (perfectClosure.comap_eq_of_algHom i).ge

Premises used: Iff.mpr, IntermediateField.map_le_iff_le_comap, Eq.ge, perfectClosure.comap_eq_of_algHom
-- 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
i : E ≃ₐ[F] K
⊢ map (↑i : E →ₐ[F] K) (perfectClosure F E) = perfectClosure F K

Tactic:
(map_le_of_algHom i.toAlgHom).antisymm (fun x hx ↦ ⟨i.symm x,
    (map_mem_perfectClosure_iff i.symm.toAlgHom).2 hx, i.right_inv x⟩)

Premises used: Iff.mpr, perfectClosure.map_le_of_algHom, Equiv.right_inv, AlgEquiv.toAlgHom, AlgEquiv.symm, map_mem_perfectClosure_iff, LE.le.antisymm, And.intro, Exists.intro, AlgEquiv.toEquiv, 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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
⊢ ExpChar F p

Tactic:
haveI := RingHom.expChar _ (algebraMap F E).injective p
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
obtain :
  ∀ (x' : E) (hx : (frobenius E p : (a : E) → E) x' = (↑x : E)),
    ∃ (a : ↥(perfectClosure F E)),
      (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x

Tactic:
obtain ⟨x', hx⟩ := surjective_frobenius E p x.1

Premises used: surjective_frobenius, Subtype.val
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : (frobenius E p : (a : E) → E) x' = (↑x : E)
obtain :
  ∀ (n : ℕ) (y : F) (hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = (↑x : E) ^ p ^ n),
    ∃ (a : ↥(perfectClosure F E)),
      (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x

Tactic:
obtain ⟨n, y, hy⟩ := (mem_perfectClosure_iff_pow_mem p).1 x.2

Premises used: mem_perfectClosure_iff_pow_mem, Iff.mp, Subtype.property
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : (frobenius E p : (a : E) → E) x' = (↑x : E)
n : ℕ
y : F
hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = (↑x : E) ^ p ^ n
rw :
  ∀ (hx : x' ^ p = (↑x : E)) (n : ℕ) (y : F) (hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = (↑x : E) ^ p ^ n),
    ∃ (a : ↥(perfectClosure F E)),
      (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x

Tactic:
rw [frobenius_def] at hx

Premises used: frobenius_def
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = (↑x : E)
n : ℕ
y : F
hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = (↑x : E) ^ p ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) y = x' ^ p ^ (n + 1)

Tactic:
rw [← hx, ← pow_mul, ← pow_succ'] at hy

Premises used: pow_mul, pow_succ'
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = (↑x : E)
n : ℕ
y : F
hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = x' ^ p ^ (n + 1)
simp_rw :
  HPow.hPow (α := ↥(perfectClosure F E))
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x) x' ⋯) p =
    x
simp_rw₁ :
  Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x) (x' ^ p) ⋯ = x
⊢ (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E))
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x) x' ⋯) =
    x

Tactic:
simp_rw [frobenius_def, SubmonoidClass.mk_pow, hx]

Premises used: SubmonoidClass.mk_pow, frobenius_def
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = (↑x : E)
n : ℕ
y : F
hy : ((algebraMap F E : F →+* E) : (a : F) → E) y = x' ^ p ^ (n + 1)
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x

Tactic:
exact ⟨⟨x', (mem_perfectClosure_iff_pow_mem p).2 ⟨n + 1, y, hy⟩⟩, by
    simp_rw [frobenius_def, SubmonoidClass.mk_pow, hx]⟩
-- 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
inst_5 : PerfectField E
⊢ PerfectField.{v} ↥(perfectClosure F E)

Tactic:
PerfectRing.toPerfectField _ (ringExpChar E)

Premises used: PerfectRing.toPerfectField, ringExpChar
-- 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 : LE.le (α := IntermediateField F E) F⟮x⟯ (perfectClosure F E) ↔ Polynomial.natSepDegree (minpoly F x) = 1
rw₁ : Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔ Polynomial.natSepDegree (minpoly F x) = 1
rw₂ rw₃ : Polynomial.natSepDegree (minpoly F x) = 1 ↔ Polynomial.natSepDegree (minpoly F x) = 1
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔ Polynomial.natSepDegree (minpoly F x) = 1

Tactic:
rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]

Premises used: mem_perfectClosure_iff_natSepDegree_eq_one, IntermediateField.adjoin_simple_le_iff, le_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
q : ℕ
hF : ExpChar F q
x : E
rw :
  LE.le (α := IntermediateField F E) F⟮x⟯ (perfectClosure F E) ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
rw₁ :
  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)
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)
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem q]

Premises used: mem_perfectClosure_iff_pow_mem, IntermediateField.adjoin_simple_le_iff, le_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
q : ℕ
hF : ExpChar F q
S : Set E
simp_rw :
  LE.le (α := IntermediateField F E) (adjoin F S) (perfectClosure F E) ↔
    ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
simp_rw₁ :
  S ⊆ (↑(perfectClosure F E) : Set E) ↔
    ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
simp_rw₂ :
  S ⊆ (↑(perfectClosure F E) : Set E) ↔ ∀ x ∈ S, Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
simp_rw₃ :
  (∀ x ∈ S, x ∈ (↑(perfectClosure F E) : Set E)) ↔
    ∀ x ∈ S, Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
⊢ IsPurelyInseparable.{u, v} F ↥(adjoin F S) ↔
    ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]

Premises used: Set.subset_def, IntermediateField.adjoin_le_iff, mem_perfectClosure_iff_pow_mem, SetLike.mem_coe, le_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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : IsPurelyInseparable.{u, v} F ↥L1
h2 : IsPurelyInseparable.{u, v} F ↥L2
rw : ∀ (h1 : L1 ≤ perfectClosure F E) (h2 : L2 ≤ perfectClosure F E), L1 ⊔ L2 ≤ perfectClosure F E
⊢ IsPurelyInseparable.{u, v} F ↥(L1 ⊔ L2)

Tactic:
rw [← le_perfectClosure_iff] at h1 h2 ⊢

Premises used: le_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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : L1 ≤ perfectClosure F E
h2 : L2 ≤ perfectClosure F E
⊢ L1 ⊔ L2 ≤ perfectClosure F E

Tactic:
sup_le h1 h2

Premises used: sup_le
-- 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
L1 L2 : IntermediateField F E
h1 : L1 ≤ perfectClosure F E
h2 : L2 ≤ perfectClosure F E
⊢ L1 ⊔ L2 ≤ perfectClosure F E

Tactic:
exact sup_le h1 h2

Premises used: sup_le
-- 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
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), IsPurelyInseparable.{u, v} F ↥(t i)
simp_rw :
  ∀ (h : ∀ (i : ι), t i ≤ perfectClosure F E), LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (perfectClosure F E)
⊢ IsPurelyInseparable.{u, v} F ↥(⨆ (i : ι), t i)

Tactic:
simp_rw [← le_perfectClosure_iff] at h ⊢

Premises used: le_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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ perfectClosure F E
⊢ LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (perfectClosure F E)

Tactic:
iSup_le h

Premises used: Set.Mem, iSup_le
-- 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
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ perfectClosure F E
⊢ LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (perfectClosure F E)

Tactic:
exact iSup_le h

Premises used: iSup_le
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
inst_3 : Algebra.IsSeparable.{u, v} F ↥(adjoin F S)
q : ℕ
inst_4 : ExpChar F q
n : ℕ
set :
  let L : IntermediateField F E := adjoin F S;
  Algebra.IsSeparable.{u, v} F ↥L → L = adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S))

Tactic:
set L := adjoin F S

Premises used: IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
set :
  let M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S);
  L = M
⊢ L = adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)

Tactic:
set M := adjoin F ((· ^ q ^ n) '' S)

Premises used: HPow.hPow, IntermediateField.adjoin, Set.image
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
rw : (fun (x : E) ↦ x ^ q ^ n) '' S ⊆ (↑L : Set E)
⊢ M ≤ L

Tactic:
rw [adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_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
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
y : E
hy : y ∈ S
⊢ (fun (x : E) ↦ x ^ q ^ n) y ∈ (↑L : Set E)

Tactic:
pow_mem (subset_adjoin F S hy) _

Premises used: Set.Mem, IntermediateField.subset_adjoin, pow_mem