-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem injective_comp_algebraMap [CommRing L] [IsReduced L] :
    Function.Injective fun f : E →+* L ↦ f.comp (algebraMap F E) := fun f g heq ↦ by
  ext x
  let q := ringExpChar F
  obtain ⟨n, y, h⟩ := IsPurelyInseparable.pow_mem F q x
  replace heq := congr($heq y)
  simp_rw [RingHom.comp_apply, h, map_pow] at heq
  nontriviality L
  haveI := expChar_of_injective_ringHom (f.comp (algebraMap F E)).injective q
  exact iterateFrobenius_inj L q n heq

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
a✝ : Nontrivial L
⊢ f x = g x

Tactic:
haveI := expChar_of_injective_ringHom (f.comp (algebraMap F E)).injective q

Result:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
a✝ : Nontrivial L
this : ExpChar L q
⊢ f x = g x

Proof state:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
⊢ f x = g x

Tactic:
let q := ringExpChar F

Result:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
q : ℕ := ringExpChar F
⊢ f x = g x

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
a✝ : Nontrivial L
this : ExpChar L q
⊢ f x = g x

Tactic:
exact iterateFrobenius_inj L q n heq

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
⊢ f = g

Tactic:
ext x

Result:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
⊢ f x = g x

Proof state:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
⊢ f x = g x

Tactic:
replace heq := congr($heq y)

Result:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : ((fun f => f.comp (algebraMap F E)) f) y = ((fun f => f.comp (algebraMap F E)) g) y
⊢ f x = g x

Proof state:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
⊢ f x = g x

Tactic:
nontriviality L

Result:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
a✝ : Nontrivial L
⊢ f x = g x

Proof state:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : ((fun f => f.comp (algebraMap F E)) f) y = ((fun f => f.comp (algebraMap F E)) g) y
⊢ f x = g x

Tactic:
simp_rw [RingHom.comp_apply, h, map_pow] at heq

Result:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f x ^ q ^ n = g x ^ q ^ n
⊢ f x = g x

Proof state:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
q : ℕ := ringExpChar F
⊢ f x = g x

Tactic:
obtain ⟨n, y, h⟩ := IsPurelyInseparable.pow_mem F q x

Result:
case a.intro.intro
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f => f.comp (algebraMap F E)) f = (fun f => f.comp (algebraMap F E)) g
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
⊢ f x = g x