-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isPurelyInseparable_of_finSepDegree_eq_one
    (hdeg : finSepDegree F E = 1) : IsPurelyInseparable F E

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E
this : F⟮x⟯ = ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range

Tactic:
simpa only [this.1] using mem_adjoin_simple_self F x

Result:
no goals

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : Algebra.IsAlgebraic (↥F⟮x⟯) E
⊢ x ∈ (algebraMap F E).range

Tactic:
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E
⊢ x ∈ (algebraMap F E).range

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E
⊢ x ∈ (algebraMap F E).range

Tactic:
rw [hdeg, mul_eq_one, (finSepDegree_adjoin_simple_eq_finrank_iff F E x
    (Algebra.IsAlgebraic.isAlgebraic x)).2 hsep,
  IntermediateField.finrank_eq_one_iff] at this

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E
this : F⟮x⟯ = ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Tactic:
refine fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hsep ↦ ?_⟩

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Tactic:
rw [isPurelyInseparable_iff]

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
have : Algebra.IsAlgebraic F⟮x⟯ E := Algebra.IsAlgebraic.tower_top (K := F) F⟮x⟯

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : Algebra.IsAlgebraic (↥F⟮x⟯) E
⊢ x ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
⊢ IsPurelyInseparable F E

Tactic:
by_cases H : Algebra.IsAlgebraic F E

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : ¬Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : ¬Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at H

Result:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.Transcendental F E
⊢ IsPurelyInseparable F E

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.Transcendental F E
⊢ IsPurelyInseparable F E

Tactic:
simp [finSepDegree_eq_zero_of_transcendental F E] at hdeg

Result:
no goals