awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
inst_9 : ExpChar F q
inst_10 : IsPurelyInseparable F E
inst_11 : FiniteDimensional F E
d : ℕ
hd : finrank F E = d
⊢ ∃ (n : ℕ), d = q ^ n
have ind : ∀ (d : ℕ)
  (IH :
    ∀ m < d,
      ∀ (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
        [FiniteDimensional F E] (hd : finrank F E = m), ∃ (n : ℕ), m = q ^ n)
  (F : Type v) [inst : Field F] [inst_12 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E]
  (hd : finrank F E = d), ∃ (n : ℕ), d = q ^ n
Tactic: induction d using Nat.strongRecOn generalizing F with
  | ind d IH =>
    by_cases h : (⊥ : IntermediateField F E) = ⊤
    · rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd
      exact ⟨0, ((pow_zero q).trans hd).symm⟩
    obtain ⟨x, -, hx⟩ := SetLike.exists_of_lt (lt_of_le_of_ne bot_le h :)
    obtain ⟨m, y, e⟩ := IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x
    have : finrank F F⟮x⟯ = q ^ m := by
      rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]
    obtain ⟨n, hn⟩ := IH _ (by
      rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
      by_contra! H
      refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
      exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne') (F⟮x⟯) rfl
    exact ⟨m + n, by rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]⟩
Cleared hypotheses: F, inst_6, inst_8, inst_9, inst_10, inst_11, d, hd
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
⊢ IsPurelyInseparable F E
have pos : ∀ (H : Algebra.IsAlgebraic F E), IsPurelyInseparable F E
Tactic: by_cases H : Algebra.IsAlgebraic F E
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hdeg : finSepDegree F E = 1
pos : ∀ (H : Algebra.IsAlgebraic F E), IsPurelyInseparable F E
⊢ IsPurelyInseparable F E
have neg : ∀ (H : ¬Algebra.IsAlgebraic F E), IsPurelyInseparable F E
Tactic: by_cases H : Algebra.IsAlgebraic F E
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ IsPurelyInseparable F E
have pos : ∀ (x : E),
  IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
Tactic: rw [isPurelyInseparable_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
have pos : ∀ (x : E) (hsep : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: refine fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hsep ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have this : finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E
Tactic: have := finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ IsPurelyInseparable F E
have H₁ : Algebra.Transcendental F E
Tactic: rw [← Algebra.transcendental_iff_not_isAlgebraic] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
⊢ f = g
have a : ∀ (x : E), Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
have 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)
Tactic: obtain ⟨n, y, h⟩ := IsPurelyInseparable.pow_mem F q x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
have 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)
Tactic: replace heq := congr($heq y)
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
have heq₁ : 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
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
have a : Nontrivial L
Tactic: nontriviality L
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : E) → L) x : L) ((g : (a : E) → L) x : L)
have this : ExpChar L q
Tactic: haveI := expChar_of_injective_ringHom (f.comp (algebraMap F E)).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ sepDegree F E = 1
have rw : Module.rank F ↥(separableClosure F E) = 1
Tactic: rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ sepDegree F E = 1
have rw₁ : Module.rank F ↥⊥ = 1
Tactic: rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ sepDegree F E = 1
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
Tactic: rw [sepDegree, separableClosure.eq_bot_of_isPurelyInseparable, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
⊢ insepDegree F E = Module.rank F E
have rw : Module.rank (↥(separableClosure F E)) E = Module.rank F E
Tactic: rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ insepDegree F E = Module.rank F E
have rw₁ : Module.rank (↥⊥) E = Module.rank F E
Tactic: rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ insepDegree F E = Module.rank F E
have rw₂ : Module.rank F E = Module.rank F E
Tactic: rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
inst : Field F
K : Type w
inst_1 : Field K
inst_2 : Algebra F K
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1
have rw : Eq (α := IntermediateField F K) (separableClosure F K) ⊤ ↔ finInsepDegree F K = 1
Tactic: rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1
have rw₁ : finrank (↥(separableClosure F K)) K = 1 ↔ finInsepDegree F K = 1
Tactic: rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1
have rw₂ : finrank (↥(separableClosure F K)) K = 1 ↔ finrank (↥(separableClosure F K)) K = 1
Tactic: rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
have 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)
Tactic: refine ⟨fun _ _ _ ↦ IsPurelyInseparable.tower_bot F _ E,
    fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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 ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
have hx : IsIntegral F x
Tactic: have hx : IsIntegral F x := Algebra.IsIntegral.isIntegral x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
have refine : IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: refine ⟨hx, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Separable (minpoly F (B := ↥F⟮x⟯) (AdjoinSimple.gen F x))
have rwa : Separable (minpoly F (↑(AdjoinSimple.gen F x) : E))
Tactic: rwa [minpoly_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have 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
Tactic: obtain ⟨y, h⟩ := (h _ (adjoin.finiteDimensional hx)).inseparable' _ <|
    show Separable (minpoly F (AdjoinSimple.gen F x)) by rwa [minpoly_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have 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))
Tactic: obtain ⟨n, h⟩ := IsPurelyInseparable.minpoly_eq_X_sub_C_pow F (ringExpChar F) x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ Splits (Polynomial.map (algebraMap F E) (minpoly F x))
have rw : (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ ringExpChar F ^ n).Splits
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
have refine : ∀ (h : 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x
have this : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
Tactic: haveI := (isSeparable_adjoin_simple_iff_isSeparable L E).2 h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
this : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
⊢ Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x
have this₁ : Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
Tactic: haveI : Algebra.IsSeparable F (restrictScalars F L⟮x⟯) := Algebra.IsSeparable.trans F L L⟮x⟯
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
this_1 : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
⊢ Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x
have hx : Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) x
Tactic: have hx : x ∈ L⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw₁ : #(Emb F ↥(separableClosure F E)) =
  Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} #(Emb (↥(separableClosure F E)) E)
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
rw₁ :
  #(Emb F ↥(separableClosure F E)) =
    Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} #(Emb (↥(separableClosure F E)) E)
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw₂ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} 1
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
rw₁ :
  #(Emb F ↥(separableClosure F E)) =
    Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} #(Emb (↥(separableClosure F E)) E)
rw₂ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} 1
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw₃ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * 1
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
rw₁ :
  #(Emb F ↥(separableClosure F E)) =
    Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} #(Emb (↥(separableClosure F E)) E)
rw₂ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} 1
rw₃ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * 1
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw₄ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E))
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]