awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
h : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
⊢ IsSeparable F x

Tactic:
exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, IntermediateField.mem_adjoin_simple_self
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hsep : IsSeparable F x
⊢ IsIntegral F x

Tactic:
have h := IsSeparable.isIntegral hsep
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
⊢ FiniteDimensional.{u, v} F ↥F⟮x⟯

Tactic:
haveI := adjoin.finiteDimensional h
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hsep : IsSeparable F x
h : IsIntegral F x
this : FiniteDimensional.{u, v} F ↥F⟮x⟯
refine_2 : finSepDegree.{u, v} F ↥F⟮x⟯ = finrank.{u, v} F ↥F⟮x⟯
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : IsSeparable F x
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯

Tactic:
rwa [← finSepDegree_eq_finrank_iff,
      finSepDegree_adjoin_simple_eq_finrank_iff F E x h.isAlgebraic]

Premises used: IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, IsIntegral.isAlgebraic, Field.finSepDegree_eq_finrank_iff
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
⊢ let f : E[X] := minpoly E x;
  f = minpoly E x

Tactic:
set f := minpoly E x with hf

Premises used: minpoly
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
⊢ FiniteDimensional.{u, v} F ↥E'

Tactic:
haveI : FiniteDimensional F E' :=
    finiteDimensional_adjoin fun x _ ↦ Algebra.IsSeparable.isIntegral F x
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X] := f.toSubring E'.toSubring ⋯
⊢ Polynomial.map (algebraMap (↥E') E) g = f

Tactic:
have h : g.map (algebraMap E' E) = f := f.map_toSubring E'.toSubring (subset_adjoin F _)
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X] := f.toSubring E'.toSubring ⋯
h : Polynomial.map (algebraMap (↥E') E) g = f
clear_value : ∀ (g : (↥E')[X]) (h : Polynomial.map (algebraMap (↥E') E) g = f), IsSeparable F x
⊢ IsSeparable F x

Tactic:
clear_value g
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
⊢ Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x

Tactic:
have hx : x ∈ E'⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
⊢ Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)

Tactic:
simpa only [← hf, ← h, aeval_map_algebraMap] using minpoly.aeval E x

Premises used: Polynomial.aeval_map_algebraMap, minpoly.aeval
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
⊢ Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)

Tactic:
have hzero : aeval x g = 0 := by
    simpa only [← hf, ← h, aeval_map_algebraMap] using minpoly.aeval E x
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
⊢ IsIntegral.{v, w} (↥E') x

Tactic:
have halg : IsIntegral E' x :=
    isIntegral_trans (R := F) (A := E) _ (IsSeparable.isIntegral hsep) |>.tower_top
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
⊢ g.Separable

Tactic:
simp only [IsSeparable, ← hf, ← h, separable_map] at hsep

Premises used: IsSeparable, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : g.Separable
⊢ Separable.{v} (R := ↥E') (minpoly (↥E') x)

Tactic:
replace hsep := hsep.of_dvd <| minpoly.dvd E' x hzero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
⊢ Algebra.IsSeparable.{u, v} F ↥E'

Tactic:
haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this : Algebra.IsSeparable.{u, v} F ↥E'
⊢ Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
⊢ FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯

Tactic:
haveI := adjoin.finiteDimensional halg
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
⊢ FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯

Tactic:
haveI : FiniteDimensional F E'⟮x⟯ := FiniteDimensional.trans F E' E'⟮x⟯
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this_4 : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
this : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
⊢ finSepDegree.{u, v} F ↥E' * finSepDegree.{v, w} ↥E' ↥(↥E')⟮x⟯ = finSepDegree.{u, w} F ↥(↥E')⟮x⟯

Tactic:
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F E' E'⟮x⟯
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this_4 : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
this_5 : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
this : finSepDegree.{u, v} F ↥E' * finSepDegree.{v, w} ↥E' ↥(↥E')⟮x⟯ = finSepDegree.{u, w} F ↥(↥E')⟮x⟯
⊢ Algebra.IsSeparable.{u, w} F ↥(↥E')⟮x⟯

Tactic:
rw [finSepDegree_eq_finrank_of_isSeparable F E',
    finSepDegree_eq_finrank_of_isSeparable E' E'⟮x⟯,
    Module.finrank_mul_finrank F E' E'⟮x⟯,
    eq_comm, finSepDegree_eq_finrank_iff F E'⟮x⟯] at this

Premises used: Membership.mem, Subtype, eq_comm, Field.finSepDegree_eq_finrank_of_isSeparable, Module.finrank_mul_finrank, IntermediateField.adjoin, Field.finSepDegree_eq_finrank_iff, Singleton.singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this_4 : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
this_5 : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable.{u, w} F ↥(↥E')⟮x⟯
⊢ Algebra.IsSeparable.{u, w} F ↥(IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯)

Tactic:
change Algebra.IsSeparable F (restrictScalars F E'⟮x⟯) at this

Premises used: IntermediateField.restrictScalars, Membership.mem, Subtype, Algebra.IsSeparable, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this_4 : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
this_5 : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable.{u, w} F ↥(IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯)
⊢ IsSeparable F x

Tactic:
isSeparable_of_mem_isSeparable F K hx

Premises used: IntermediateField.isSeparable_of_mem_isSeparable
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F (↑f.coeffs : Set E)
this_1 : FiniteDimensional.{u, v} F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : Membership.mem (γ := IntermediateField F K) (IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯) x
hzero : Eq.{w + 1} (α := K) ((aeval x : (a : (↥E')[X]) → K) g : K) (0 : K)
halg : IsIntegral.{v, w} (↥E') x
hsep : Separable.{v} (R := ↥E') (minpoly (↥E') x)
this_2 : Algebra.IsSeparable.{u, v} F ↥E'
this_3 : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
this_4 : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
this_5 : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable.{u, w} F ↥(IntermediateField.restrictScalars.{u, w, v} F (L' := ↥E') (↥E')⟮x⟯)
⊢ IsSeparable F x

Tactic:
exact isSeparable_of_mem_isSeparable F K hx

Premises used: IntermediateField.isSeparable_of_mem_isSeparable
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
inst_8 : Algebra.IsSeparable E K
⊢ Algebra.IsSeparable F K

Tactic:
⟨fun x ↦ IsSeparable.of_algebra_isSeparable_of_isSeparable F
    (Algebra.IsSeparable.isSeparable E x)⟩

Premises used: Algebra.IsSeparable.isSeparable, IsSeparable.of_algebra_isSeparable_of_isSeparable, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
rw : Algebra.IsSeparable.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x, y⟯

Tactic:
rw [← adjoin_simple_adjoin_simple]

Premises used: IntermediateField.adjoin_simple_adjoin_simple
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ IsSeparable (↥F⟮x⟯) y

Tactic:
replace hy := IsSeparable.tower_top F⟮x⟯ hy
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable (↥F⟮x⟯) y
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯

Tactic:
rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy

Premises used: IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable (↥F⟮x⟯) y
hx₁ : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
⊢ Algebra.IsSeparable.{v, v} ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯

Tactic:
rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy

Premises used: IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
hy : Algebra.IsSeparable.{v, v} ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
⊢ Algebra.IsSeparable.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)

Tactic:
Algebra.IsSeparable.trans F F⟮x⟯ F⟮x⟯⟮y⟯

Premises used: IntermediateField.restrictScalars, iInf, Submonoid.copy, Set.Mem, Set.iInter, Membership.mem, Subtype, IntermediateField.adjoin, RingHom.codRestrict, Singleton.singleton, Algebra.IsSeparable.trans
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
hy : Algebra.IsSeparable.{v, v} ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
⊢ Algebra.IsSeparable.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)

Tactic:
exact Algebra.IsSeparable.trans F F⟮x⟯ F⟮x⟯⟮y⟯

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, Algebra.IsSeparable.trans
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ IsSeparable F (x * y)

Tactic:
haveI := isSeparable_adjoin_pair_of_isSeparable F E hx hy
  isSeparable_of_mem_isSeparable F E <| F⟮x, y⟯.mul_mem (subset_adjoin F _ (.inl rfl))
    (subset_adjoin F _ (.inr rfl))

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, Insert.insert, IntermediateField.subset_adjoin, IntermediateField.adjoin, IntermediateField.mul_mem, Or.inl, Singleton.singleton, Or.inr, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ IsSeparable F (x + y)

Tactic:
haveI := isSeparable_adjoin_pair_of_isSeparable F E hx hy
  isSeparable_of_mem_isSeparable F E <| F⟮x, y⟯.add_mem (subset_adjoin F _ (.inl rfl))
    (subset_adjoin F _ (.inr rfl))

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, IntermediateField.add_mem, Insert.insert, IntermediateField.subset_adjoin, IntermediateField.adjoin, Or.inl, Singleton.singleton, Or.inr, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : IsSeparable F x
⊢ IsSeparable F (-x)

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).2 hx
  isSeparable_of_mem_isSeparable F E <| F⟮x⟯.neg_mem <| mem_adjoin_simple_self F x

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, IntermediateField.mem_adjoin_simple_self, IntermediateField.neg_mem, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ IsSeparable F (x - y)

Tactic:
haveI := isSeparable_adjoin_pair_of_isSeparable F E hx hy
  isSeparable_of_mem_isSeparable F E <| F⟮x, y⟯.sub_mem (subset_adjoin F _ (.inl rfl))
    (subset_adjoin F _ (.inr rfl))

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, Insert.insert, IntermediateField.subset_adjoin, IntermediateField.sub_mem, IntermediateField.adjoin, Or.inl, Singleton.singleton, Or.inr, rfl
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : IsSeparable F x
⊢ IsSeparable F x⁻¹

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).2 hx
  isSeparable_of_mem_isSeparable F E <| F⟮x⟯.inv_mem <| mem_adjoin_simple_self F x

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, IntermediateField.mem_adjoin_simple_self, IntermediateField.adjoin, IntermediateField.inv_mem, Singleton.singleton