awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E
⊢ Eq (α := IntermediateField F E) F⟮x⟯ ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1

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

Premises used: Iff.mpr, Algebra.IsAlgebraic.isAlgebraic, IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, IntermediateField.finrank_eq_one_iff, mul_eq_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : Eq (α := IntermediateField F E) F⟮x⟯ ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

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

Premises used: IntermediateField.mem_adjoin_simple_self, And.left
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
H : ¬Algebra.IsAlgebraic F E
⊢ Algebra.Transcendental F E

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at H

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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

Premises used: Field.finSepDegree_eq_zero_of_transcendental
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
heq :
  Eq (α := F →+* L) ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) f)
    ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) g)
a : ∀ (x : E), Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
heq :
  Eq (α := F →+* L) ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) f)
    ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) g)
x : E
q : ℕ := ringExpChar F
a :
  ∀ (n : ℕ) (y : F) (h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n),
    Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)

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

Premises used: IsPurelyInseparable.pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
heq :
  Eq (α := F →+* L) ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) f)
    ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) g)
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
⊢ Eq.{u_2 + 1} (α := L) (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) f : (a : F) → L) y : L)
    (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) g : (a : F) → L) y : L)

Tactic:
replace heq := congr($heq y)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
heq :
  Eq.{u_2 + 1} (α := L) (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) f : (a : F) → L) y : L)
    (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) g : (a : F) → L) y : L)
⊢ HPow.hPow (α := L) ((f : (a : E) → L) x : L) (q ^ n) = HPow.hPow (α := L) ((g : (a : E) → L) x : L) (q ^ n)

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

Premises used: map_pow, RingHom.comp_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
heq : HPow.hPow (α := L) ((f : (a : E) → L) x : L) (q ^ n) = HPow.hPow (α := L) ((g : (a : E) → L) x : L) (q ^ n)
⊢ Nontrivial L

Tactic:
nontriviality L
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
heq : HPow.hPow (α := L) ((f : (a : E) → L) x : L) (q ^ n) = HPow.hPow (α := L) ((g : (a : E) → L) x : L) (q ^ n)
h_1 : Nontrivial L
⊢ ExpChar L q

Tactic:
haveI := expChar_of_injective_ringHom (f.comp (algebraMap F E)).injective q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
heq : HPow.hPow (α := L) ((f : (a : E) → L) x : L) (q ^ n) = HPow.hPow (α := L) ((g : (a : E) → L) x : L) (q ^ n)
h_1 : Nontrivial L
this : ExpChar L q
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)

Tactic:
iterateFrobenius_inj L q n heq

Premises used: iterateFrobenius_inj
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : CommRing L
inst_5 : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : ((algebraMap F E : F →+* E) : (a : F) → E) y = x ^ q ^ n
heq : HPow.hPow (α := L) ((f : (a : E) → L) x : L) (q ^ n) = HPow.hPow (α := L) ((g : (a : E) → L) x : L) (q ^ n)
h_1 : Nontrivial L
this : ExpChar L q
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)

Tactic:
exact iterateFrobenius_inj L q n heq

Premises used: iterateFrobenius_inj
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
R : Type u_1
L : Type u_2
inst_4 : CommSemiring R
inst_5 : Algebra R F
inst_6 : Algebra R E
inst_7 : CommRing L
inst_8 : IsReduced L
inst_9 : Algebra R L
inst_10 : IsScalarTower R F E
⊢ Function.Injective (α := E →ₐ[R] L) (β := F →ₐ[R] L) (AlgHom.restrictDomain F)

Tactic:
fun _ _ eq ↦
  AlgHom.coe_ringHom_injective <| injective_comp_algebraMap F E L <| congr_arg AlgHom.toRingHom eq

Premises used: AlgHom.coe_ringHom_injective, IsPurelyInseparable.injective_comp_algebraMap, congr_arg, AlgHom.toRingHom, Function.Injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
R : Type u_1
L : Type u_2
inst_6 : CommSemiring R
inst_7 : Algebra R F
inst_8 : Algebra R E
inst_9 : Field L
inst_10 : PerfectField L
inst_11 : Algebra F L
⊢ Nonempty (E →ₐ[F] L)

Tactic:
nonempty_algHom_of_splits fun x ↦ ⟨IsPurelyInseparable.isIntegral' _ _,
    have ⟨q, _⟩ := ExpChar.exists F
    PerfectField.splits_of_natSepDegree_eq_one (algebraMap F L)
      ((minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).mpr <|
        IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x)⟩

Premises used: Iff.mpr, _private.0.IsPurelyInseparable.instNonemptyAlgHomOfPerfectField.match_1, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, Algebra.algebraMap, IsPurelyInseparable.isIntegral', minpoly, PerfectField.splits_of_natSepDegree_eq_one, And.intro, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, Polynomial.map, IntermediateField.nonempty_algHom_of_splits, Polynomial.Splits, ExpChar.exists
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
L : Type u_2
inst_4 : Field L
inst_5 : PerfectField L
⊢ Function.Bijective (β := F →+* L) fun (f : E →+* L) ↦ f.comp (algebraMap F E)

Tactic:
⟨injective_comp_algebraMap F E L, fun g ↦ let _ := g.toAlgebra
    ⟨_, (Classical.arbitrary <| E →ₐ[F] L).comp_algebraMap⟩⟩

Premises used: AlgHom.comp_algebraMap, AlgHom, IsPurelyInseparable.injective_comp_algebraMap, RingHomClass.toRingHom, And.intro, Exists.intro, Classical.arbitrary, Function.Bijective, RingHom.toAlgebra
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
R : Type u_1
L : Type u_2
inst_4 : CommSemiring R
inst_5 : Algebra R F
inst_6 : Algebra R E
inst_7 : Field L
inst_8 : PerfectField L
inst_9 : Algebra R L
inst_10 : IsScalarTower R F E
⊢ Function.Bijective (α := E →ₐ[R] L) (β := F →ₐ[R] L) (AlgHom.restrictDomain F)

Tactic:
⟨injective_restrictDomain F E R L, fun g ↦ let _ := g.toAlgebra
    let f := Classical.arbitrary (E →ₐ[F] L)
    ⟨f.restrictScalars R, AlgHom.coe_ringHom_injective f.comp_algebraMap⟩⟩

Premises used: AlgHom.coe_ringHom_injective, AlgHom.comp_algebraMap, AlgHom, AlgHom.restrictScalars, AlgHom.toRingHom, IsPurelyInseparable.injective_restrictDomain, And.intro, Exists.intro, Classical.arbitrary, Function.Bijective, RingHom.toAlgebra
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
L : Type w
inst_6 : CommRing L
inst_7 : IsReduced L
inst_8 : Algebra F L
f g : E →ₐ[F] L
simp_rw simp_rw₁ :
  Eq (α := F →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : E →+* L) (algebraMap F E))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : E →+* L) (algebraMap F E))
⊢ Eq (α := F →+* L) ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (↑f : E →+* L))
    ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (↑g : E →+* L))

Tactic:
simp_rw [AlgHom.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ finSepDegree F E = 1

Tactic:
Nat.card_unique

Premises used: Field.finSepDegree, Nat.card_unique
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
rw : Module.rank F ↥(separableClosure F E) = 1
rw₁ : Module.rank F ↥⊥ = 1
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
⊢ sepDegree F E = 1

Tactic:
rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]

Premises used: Field.sepDegree, IntermediateField.rank_bot, separableClosure.eq_bot_of_isPurelyInseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
rw : Module.rank (↥(separableClosure F E)) E = Module.rank F E
rw₁ : Module.rank (↥⊥) E = Module.rank F E
rw₂ rw₃ : Module.rank F E = Module.rank F E
⊢ insepDegree F E = Module.rank F E

Tactic:
rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']

Premises used: Field.insepDegree, IntermediateField.rank_bot', separableClosure.eq_bot_of_isPurelyInseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ finInsepDegree F E = finrank F E

Tactic:
congr(Cardinal.toNat $(insepDegree_eq F E))

Premises used: IsPurelyInseparable.insepDegree_eq, congrArg, Cardinal.toNat, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsPurelyInseparable F E ↔ finSepDegree F E = 1

Tactic:
⟨fun _ ↦ IsPurelyInseparable.finSepDegree_eq_one F E,
    fun h ↦ isPurelyInseparable_of_finSepDegree_eq_one h⟩

Premises used: isPurelyInseparable_of_finSepDegree_eq_one, Iff.intro, IsPurelyInseparable.finSepDegree_eq_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
inst : Field F
K : Type w
inst_1 : Field K
inst_2 : Algebra F K
rw : Eq (α := IntermediateField F K) (separableClosure F K) ⊤ ↔ finInsepDegree F K = 1
rw₁ : finrank (↥(separableClosure F K)) K = 1 ↔ finInsepDegree F K = 1
rw₂ rw₃ : finrank (↥(separableClosure F K)) K = 1 ↔ finrank (↥(separableClosure F K)) K = 1
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1

Tactic:
rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]

Premises used: Field.finInsepDegree, separableClosure.eq_top_iff, IntermediateField.finrank_eq_one_iff_eq_top
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E ↔
    ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L

Tactic:
⟨fun _ _ _ ↦ IsPurelyInseparable.tower_bot F _ E,
    fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ?_⟩

Premises used: Iff.mpr, Membership.mem, Subtype, IsPurelyInseparable.tower_bot, isPurelyInseparable_iff, Iff.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
refine :
  ∀ (h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L) (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
⊢ IsPurelyInseparable F E ↔
    ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L

Tactic:
refine ⟨fun _ _ _ ↦ IsPurelyInseparable.tower_bot F _ E,
    fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
⊢ IsIntegral F x

Tactic:
have hx : IsIntegral F x := Algebra.IsIntegral.isIntegral x
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)

Tactic:
⟨hx, fun _ ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
refine : IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)

Tactic:
refine ⟨hx, fun _ ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
h_1 : IsSeparable F x
rwa rwa₁ rwa₂ rwa₃ : Separable (minpoly F (↑(AdjoinSimple.gen F x) : E))
⊢ Separable (minpoly F (B := ↥F⟮x⟯) (AdjoinSimple.gen F x))

Tactic:
rwa [minpoly_eq]

Premises used: IntermediateField.minpoly_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
h_1 : IsSeparable F x
obtain :
  ∀ (y : F)
    (h :
      Eq.{v + 1} (α := ↥F⟮x⟯) (((algebraMap F ↥F⟮x⟯ : RingHom.{u, v} F ↥F⟮x⟯) : (a : F) → ↥F⟮x⟯) y : ↥F⟮x⟯)
        (AdjoinSimple.gen F x : ↥F⟮x⟯)),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
obtain ⟨y, h⟩ := (h _ (adjoin.finiteDimensional hx)).inseparable' _ <|
    show Separable (minpoly F (AdjoinSimple.gen F x)) by rwa [minpoly_eq]

Premises used: IsPurelyInseparable.inseparable'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h_1 : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
h_2 : IsSeparable F x
y : F
h :
  Eq.{v + 1} (α := ↥F⟮x⟯) (((algebraMap F ↥F⟮x⟯ : RingHom.{u, v} F ↥F⟮x⟯) : (a : F) → ↥F⟮x⟯) y : ↥F⟮x⟯)
    (AdjoinSimple.gen F x : ↥F⟮x⟯)
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
⟨y, congr_arg (algebraMap _ E) h⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, congr_arg, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h_1 : ∀ (L : IntermediateField F E), FiniteDimensional.{u, v} F ↥L → IsPurelyInseparable.{u, v} F ↥L
x : E
hx : IsIntegral F x
h_2 : IsSeparable F x
y : F
h :
  Eq.{v + 1} (α := ↥F⟮x⟯) (((algebraMap F ↥F⟮x⟯ : RingHom.{u, v} F ↥F⟮x⟯) : (a : F) → ↥F⟮x⟯) y : ↥F⟮x⟯)
    (AdjoinSimple.gen F x : ↥F⟮x⟯)
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
exact ⟨y, congr_arg (algebraMap _ E) h⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
x : E
obtain :
  ∀ (n : ℕ)
    (h :
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n),
    Splits (Polynomial.map (algebraMap F E) (minpoly F x))
⊢ Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
obtain ⟨n, h⟩ := IsPurelyInseparable.minpoly_eq_X_sub_C_pow F (ringExpChar F) x

Premises used: ringExpChar, IsPurelyInseparable.minpoly_eq_X_sub_C_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
x : E
n : ℕ
h :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n
rw : (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n).Splits
⊢ Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
x : E
n : ℕ
h :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n).Splits

Tactic:
Splits.pow (Splits.X_sub_C _) _

Premises used: Polynomial.Splits.pow, Polynomial.Splits.X_sub_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 : IsPurelyInseparable F E
x : E
n : ℕ
h :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n
⊢ (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n).Splits

Tactic:
exact Splits.pow (Splits.X_sub_C _) _

Premises used: Polynomial.Splits.pow, Polynomial.Splits.X_sub_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
set :
  let L : IntermediateField F E := separableClosure F E;
  IsIntegral (↥L) x ∧
    (IsSeparable (↥L) x → Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x)
⊢ IsIntegral (↥(separableClosure F E)) x ∧
    (IsSeparable (↥(separableClosure F E)) x →
      Membership.mem (γ := Subring E)
        (RingHom.range (R := ↥(separableClosure F E)) (algebraMap (↥(separableClosure F E)) E)) x)

Tactic:
set L := separableClosure F E

Premises used: separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
⊢ IsIntegral (↥L) x ∧
    (IsSeparable (↥L) x → Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x)

Tactic:
⟨(IsAlgebraic.tower_top L (Algebra.IsAlgebraic.isAlgebraic (R := F) x)).isIntegral,
    fun h ↦ ?_⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.tower_top, Membership.mem, Subtype, And.intro, IsAlgebraic.isIntegral
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
refine : ∀ (h : IsSeparable (↥L) x), Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x
⊢ IsIntegral (↥L) x ∧
    (IsSeparable (↥L) x → Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x)

Tactic:
refine ⟨(IsAlgebraic.tower_top L (Algebra.IsAlgebraic.isAlgebraic (R := F) x)).isIntegral,
    fun h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
⊢ Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable L E).2 h