awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ ringExpChar F ^ n
have 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)
Tactic: apply_fun i using i.injective
-- 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
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)
⊢ 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)
have refine_1 : Eq.{w + 1} (α := K) ((algebraMap F K : (a : F) → K) y : K) ((i : (a : E) → K) (x ^ ringExpChar F ^ n) : K)
Tactic: rwa [AlgHom.commutes, map_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
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
⊢ comap i (perfectClosure F K) = perfectClosure F E
have h : ∀ (x : E), x ∈ comap i (perfectClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
Tactic: ext x
-- 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
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)
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
have this : ExpChar F p
Tactic: haveI := RingHom.expChar _ (algebraMap F E).injective p
-- 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
p : ℕ
inst_5 : ExpChar E p
inst_6 : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
have 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
Tactic: obtain ⟨x', hx⟩ := surjective_frobenius E p x.1
-- 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
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)
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
have 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
Tactic: obtain ⟨n, y, hy⟩ := (mem_perfectClosure_iff_pow_mem p).1 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
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
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
have 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
Tactic: rw [frobenius_def] at hx
Cleared hypotheses: hx, n, y, hy
-- 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
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
⊢ ∃ (a : ↥(perfectClosure F E)),
    (frobenius (↥(perfectClosure F E)) p : (a : ↥(perfectClosure F E)) → ↥(perfectClosure F E)) a = x
have hy₁ : ((algebraMap F E : F →+* E) : (a : F) → E) y = x' ^ p ^ (n + 1)
Tactic: rw [← hx, ← pow_mul, ← pow_succ'] at hy
Cleared hypotheses: hy
-- 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
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)
⊢ (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
have simp_rw : HPow.hPow (α := ↥(perfectClosure F E))
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x) x' sorry) p =
  x
Tactic: simp_rw [frobenius_def, SubmonoidClass.mk_pow, 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
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
⊢ (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
have simp_rw₁ : Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x) (x' ^ p) sorry = x
Tactic: simp_rw [frobenius_def, SubmonoidClass.mk_pow, 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
x : E
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔ Polynomial.natSepDegree (minpoly F x) = 1
have rw : LE.le (α := IntermediateField F E) F⟮x⟯ (perfectClosure F E) ↔ Polynomial.natSepDegree (minpoly F x) = 1
Tactic: rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]
-- 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 : LE.le (α := IntermediateField F E) F⟮x⟯ (perfectClosure F E) ↔ Polynomial.natSepDegree (minpoly F x) = 1
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔ Polynomial.natSepDegree (minpoly F x) = 1
have rw₁ : Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x ↔ Polynomial.natSepDegree (minpoly F x) = 1
Tactic: rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]
-- 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 : 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
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔ Polynomial.natSepDegree (minpoly F x) = 1
have rw₂ : Polynomial.natSepDegree (minpoly F x) = 1 ↔ Polynomial.natSepDegree (minpoly F x) = 1
Tactic: rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_natSepDegree_eq_one]
-- 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 : ℕ
hF : ExpChar F q
x : E
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have 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)
Tactic: rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem 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 : ℕ
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)
⊢ IsPurelyInseparable.{u, v} F ↥F⟮x⟯ ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have 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)
Tactic: rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem 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 : ℕ
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)
⊢ IsPurelyInseparable.{u, v} F ↥F⟮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 [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem 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 : ℕ
hF : ExpChar F q
S : Set E
⊢ 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)
have 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)
Tactic: simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]
-- 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 : ℕ
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)
⊢ 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)
have 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)
Tactic: simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]
-- 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 : ℕ
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)
⊢ 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)
have simp_rw₂ : S ⊆ (↑(perfectClosure F E) : Set E) ↔ ∀ x ∈ S, Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
Tactic: simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]
-- 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 : ℕ
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
⊢ 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)
have simp_rw₃ : (∀ x ∈ S, x ∈ (↑(perfectClosure F E) : Set E)) ↔
  ∀ x ∈ S, Membership.mem (γ := IntermediateField F E) (perfectClosure F E) x
Tactic: simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]
-- 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
L1 L2 : IntermediateField F E
h1 : IsPurelyInseparable.{u, v} F ↥L1
h2 : IsPurelyInseparable.{u, v} F ↥L2
⊢ IsPurelyInseparable.{u, v} F ↥(L1 ⊔ L2)
have rw : ∀ (h1 : L1 ≤ perfectClosure F E) (h2 : L2 ≤ perfectClosure F E), L1 ⊔ L2 ≤ perfectClosure F E
Tactic: rw [← le_perfectClosure_iff] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- 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
ι : Sort u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), IsPurelyInseparable.{u, v} F ↥(t i)
⊢ IsPurelyInseparable.{u, v} F ↥(⨆ (i : ι), t i)
have simp_rw : ∀ (h : ∀ (i : ι), t i ≤ perfectClosure F E), LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (perfectClosure F E)
Tactic: simp_rw [← le_perfectClosure_iff] 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
S : Set E
inst_3 : Algebra.IsSeparable.{u, v} F ↥(adjoin F S)
q : ℕ
inst_4 : ExpChar F q
n : ℕ
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S))
have 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)
Tactic: set L := adjoin F S
Cleared hypotheses: inst_3
-- 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
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)
⊢ M ≤ L
have rw : (fun (x : E) ↦ x ^ q ^ n) '' S ⊆ (↑L : Set E)
Tactic: rw [adjoin_le_iff]
-- 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
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)
⊢ L = M
have hi : M ≤ L
Tactic: have hi : M ≤ L := by
    rw [adjoin_le_iff]
    rintro _ ⟨y, hy, rfl⟩
    exact pow_mem (subset_adjoin F S hy) _
-- 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
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)
hi : M ≤ L
this : Algebra ↥M ↥L := (inclusion hi).toAlgebra
⊢ L = M
have this₁ : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
Tactic: haveI : Algebra.IsSeparable M (extendScalars hi) :=
    Algebra.isSeparable_tower_top_of_isSeparable F M 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
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)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
⊢ IsPurelyInseparable.{v, v} ↥M ↥(extendScalars hi)
have rw : ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range (R := ↥M) (algebraMap (↥M) E)) (x ^ q ^ n)
Tactic: rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]
-- 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
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)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
⊢ L = M
have this₁ : IsPurelyInseparable.{v, v} ↥M ↥(extendScalars hi)
Tactic: haveI : IsPurelyInseparable M (extendScalars hi) := by
    rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]
    exact fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩
-- 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
a : E
ha : IsSeparable F a
q : ℕ
inst_3 : ExpChar F q
n : ℕ
⊢ Eq (α := IntermediateField F E) F⟮a⟯ F⟮a ^ q ^ n⟯
have this : Algebra.IsSeparable.{u, v} F ↥F⟮a⟯
Tactic: haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).mpr ha
-- 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 n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
⊢ Eq.{v + 1} (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n)) ⊤
have rw : Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
  (Submodule.span F (↑(Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n)) : Set E))
Tactic: rw [← Algebra.top_toSubmodule, ← top_toSubalgebra, ← adjoin_univ,
    adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,
    adjoin_toSubalgebra_of_isAlgebraic fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x,
    Set.image_univ, Algebra.adjoin_eq_span]
-- 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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F (↑(Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n)) : Set E))
have this : Eq (α := Submonoid E) (Submonoid.closure (↑(MonoidHom.mrange (F := E →* E) (powMonoidHom (q ^ n))) : Set E))
  (MonoidHom.mrange (F := E →* E) (powMonoidHom (q ^ n)))
Tactic: have := (MonoidHom.mrange (powMonoidHom (α := E) (q ^ n))).closure_eq
-- 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 n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
this :
  Eq (α := Submonoid E) (Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n))
    (Submonoid.copy (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤)
      (Set.range fun (x : E) ↦ x ^ q ^ n) ⋯)
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F (↑(Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n)) : Set E))
have rw : Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
  (Submodule.span F
    (↑(Submonoid.copy (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := sorry, map_mul' := sorry } ⊤)
          (Set.range fun (x : E) ↦ x ^ q ^ n) sorry) :
      Set E))
Tactic: rw [this]
-- 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 n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
this :
  Eq (α := Submonoid E) (Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n))
    (Submonoid.copy (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤)
      (Set.range fun (x : E) ↦ x ^ q ^ n) ⋯)
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F
      (↑(Submonoid.copy
            (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤)
            (Set.range fun (x : E) ↦ x ^ q ^ n) ⋯) :
        Set E))
have refine : Set.range (ι := E) ((Semiring.toMonoid : Monoid E).5 (q ^ n)) ⊆
  (↑(Submodule.span F (Set.range ((Semiring.toMonoid : Monoid E).5 (q ^ n) ∘ v))) : Set E)
Tactic: refine (Submodule.span_mono <| Set.range_comp_subset_range _ _).antisymm (Submodule.span_le.2 ?_)