-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable (S : Set E)
    [Algebra.IsSeparable F (adjoin F S)] (q : ℕ) [ExpChar F q] (n : ℕ) :
    adjoin F S = adjoin F ((· ^ q ^ n) '' S)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
⊢ L = M

Tactic:
have hi : M ≤ L := by
  rw [adjoin_le_iff]
  rintro _ ⟨y, hy, rfl⟩
  exact pow_mem (subset_adjoin F S hy) _

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
⊢ L = M

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
y : E
hy : y ∈ S
⊢ (fun x => x ^ q ^ n) y ∈ ↑L

Tactic:
exact pow_mem (subset_adjoin F S hy) _

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable ↥M ↥(extendScalars hi)
⊢ L = M

Tactic:
haveI : IsPurelyInseparable M (extendScalars hi) := by
  haveI := expChar_of_injective_algebraMap (algebraMap F M).injective q
  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⟩

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : IsPurelyInseparable ↥M ↥(extendScalars hi)
⊢ L = M

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
⊢ (fun x => x ^ q ^ n) '' S ⊆ ↑L

Tactic:
rintro _ ⟨y, hy, rfl⟩

Result:
case intro.intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
y : E
hy : y ∈ S
⊢ (fun x => x ^ q ^ n) y ∈ ↑L

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : ExpChar (↥M) q
⊢ IsPurelyInseparable ↥M ↥(extendScalars hi)

Tactic:
rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : ExpChar (↥M) q
⊢ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap (↥M) E).range

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
⊢ L = M

Tactic:
letI := (inclusion hi).toAlgebra

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this : Algebra ↥M ↥L := (inclusion hi).toAlgebra
⊢ L = M

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : IsPurelyInseparable ↥M ↥(extendScalars hi)
⊢ L = M

Tactic:
simpa only [extendScalars_restrictScalars, restrictScalars_bot_eq_self] using congr_arg
  (restrictScalars F) (extendScalars hi).eq_bot_of_isPurelyInseparable_of_isSeparable

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : ExpChar (↥M) q
⊢ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap (↥M) E).range

Tactic:
exact fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
⊢ M ≤ L

Tactic:
rw [adjoin_le_iff]

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
⊢ (fun x => x ^ q ^ n) '' S ⊆ ↑L

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ adjoin F S = adjoin F ((fun x => x ^ q ^ n) '' S)

Tactic:
set L := adjoin F S

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
⊢ L = adjoin F ((fun x => x ^ q ^ n) '' S)