-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem IsPurelyInseparable.of_injective_comp_algebraMap (L : Type w) [Field L] [IsAlgClosed L]
    [Nonempty (E →+* L)] (h : Function.Injective fun f : E →+* L ↦ f.comp (algebraMap F E)) :
    IsPurelyInseparable F E

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ (fun f => f.comp (algebraMap F E)) (j.comp ↑f) = (fun f => f.comp (algebraMap F E)) (j.comp ↑g)

Tactic:
ext

Result:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
x✝ : F
⊢ ((fun f => f.comp (algebraMap F E)) (j.comp ↑f)) x✝ = ((fun f => f.comp (algebraMap F E)) (j.comp ↑g)) x✝

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Tactic:
exact ⟨⟨fun f g ↦ DFunLike.ext' <| j.injective.comp_left (congr_arg (⇑) <|
  @h (j.toRingHom.comp f) (j.toRingHom.comp g) (by ext; simp))⟩, inferInstance⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Tactic:
letI := (Classical.arbitrary (E →+* L)).toAlgebra

Result:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Tactic:
let j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift

Result:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Proof state:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
⊢ IsPurelyInseparable F E

Tactic:
rw [isPurelyInseparable_iff_finSepDegree_eq_one, finSepDegree, Nat.card_eq_one_iff_unique]

Result:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
⊢ Subsingleton (Emb F E) ∧ Nonempty (Emb F E)

Proof state:
case a
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f => f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
x✝ : F
⊢ ((fun f => f.comp (algebraMap F E)) (j.comp ↑f)) x✝ = ((fun f => f.comp (algebraMap F E)) (j.comp ↑g)) x✝

Tactic:
simp

Result:
no goals