-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem perfectField_of_perfectClosure_eq_bot [h : PerfectField E] (eq : perfectClosure F E = ⊥) :
    PerfectField F

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
⊢ (algebraMap F E) x = y ^ ringExpChar F ^ 1

Tactic:
rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]

Result:
no goals

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((Algebra.ofId F E).toRingHom z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x

Tactic:
exact ⟨z, (algebraMap F E).injective (by erw [RingHom.map_frobenius, h])⟩

Result:
no goals

Proof state:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
⊢ ∃ a, (frobenius F p) a = x

Tactic:
have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩

Result:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
this : y ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
⊢ PerfectField F

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective p

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
⊢ PerfectField F

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((Algebra.ofId F E).toRingHom z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ (algebraMap F E) ((frobenius F p) z) = (algebraMap F E) x

Tactic:
erw [RingHom.map_frobenius, h]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
exact PerfectRing.toPerfectField F p

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
⊢ ∃ a, (frobenius F p) a = x

Tactic:
obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)

Result:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
⊢ ∃ a, (frobenius F p) a = x

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
⊢ PerfectField F

Tactic:
haveI := PerfectRing.ofSurjective F p fun x ↦ by
  obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
  have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
  obtain ⟨z, rfl⟩ := eq ▸ this
  exact ⟨z, (algebraMap F E).injective (by erw [RingHom.map_frobenius, h])⟩

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
this : PerfectRing F p
⊢ PerfectField F

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
⊢ PerfectField F

Tactic:
let p := ringExpChar F

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
⊢ PerfectField F

Proof state:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
this : y ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x

Tactic:
obtain ⟨z, rfl⟩ := eq ▸ this

Result:
case intro.intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((Algebra.ofId F E).toRingHom z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ ∃ a, (frobenius F p) a = x