awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
⊢ False
have this : finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank.{u, v} F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
Tactic: have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.pos'
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
this : finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank.{u, v} F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ False
have this₁ : finSepDegree F E < finrank F E
Tactic: rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E,
      Module.finrank_mul_finrank F F⟮x⟯ E] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
⊢ False
have linarith : -1 + -HSub.hSub (α := ℤ) (↑(finSepDegree F E) : ℤ) (↑(finrank F E) : ℤ) +
    (HAdd.hAdd (α := ℤ) (↑(finSepDegree F E) : ℤ) 1 - (↑(finrank F E) : ℤ)) =
  0
Tactic: linarith only [heq, this]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ ↔ IsSeparable F x
have refine_1 : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ → IsSeparable F x
Tactic: refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
refine_1 : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ → IsSeparable F x
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ ↔ IsSeparable F x
have refine_2 : ∀ (hsep : IsSeparable F x), Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
Tactic: refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
have h : IsIntegral F x
Tactic: have h := IsSeparable.isIntegral hsep
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
have this : FiniteDimensional.{u, v} F ↥F⟮x⟯
Tactic: haveI := adjoin.finiteDimensional h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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⟯
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
have refine_2 : finSepDegree.{u, v} F ↥F⟮x⟯ = finrank.{u, v} F ↥F⟮x⟯
Tactic: rwa [← finSepDegree_eq_finrank_iff,
      finSepDegree_adjoin_simple_eq_finrank_iff F E x h.isAlgebraic]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
⊢ IsSeparable F x
have hf : let f : E[X] := minpoly E x;
f = minpoly E x
Tactic: set f := minpoly E x with hf
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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)
⊢ IsSeparable F x
have this : FiniteDimensional.{u, v} F ↥E'
Tactic: haveI : FiniteDimensional F E' :=
    finiteDimensional_adjoin fun x _ ↦ Algebra.IsSeparable.isIntegral F x
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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 ⋯
⊢ IsSeparable F x
have h : Polynomial.map (algebraMap (↥E') E) g = f
Tactic: have h : g.map (algebraMap E' E) = f := f.map_toSubring E'.toSubring (subset_adjoin F _)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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
⊢ IsSeparable F x
have clear_value : ∀ (g : (↥E')[X]) (h : Polynomial.map (algebraMap (↥E') E) g = f), IsSeparable F x
Tactic: clear_value g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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
⊢ IsSeparable F x
have hx : 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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
⊢ IsSeparable F x
have hzero : 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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)
⊢ IsSeparable F x
have halg : IsIntegral.{v, w} (↥E') x
Tactic: have halg : IsIntegral E' x :=
    isIntegral_trans (R := F) (A := E) _ (IsSeparable.isIntegral hsep) |>.tower_top
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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
⊢ IsSeparable F x
have hsep₁ : g.Separable
Tactic: simp only [IsSeparable, ← hf, ← h, separable_map] at hsep
Cleared hypotheses: hsep
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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
⊢ IsSeparable F x
have hsep₁ : Separable.{v} (R := ↥E') (minpoly (↥E') x)
Tactic: replace hsep := hsep.of_dvd <| minpoly.dvd E' x hzero
Cleared hypotheses: hsep
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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)
⊢ IsSeparable F x
have this₁ : Algebra.IsSeparable.{u, v} F ↥E'
Tactic: haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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'
⊢ IsSeparable F x
have this₁ : Algebra.IsSeparable.{v, w} ↥E' ↥(↥E')⟮x⟯
Tactic: haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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⟯
⊢ IsSeparable F x
have this₁ : FiniteDimensional.{v, w} ↥E' ↥(↥E')⟮x⟯
Tactic: haveI := adjoin.finiteDimensional halg
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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⟯
⊢ IsSeparable F x
have this₁ : FiniteDimensional.{u, w} F ↥(↥E')⟮x⟯
Tactic: haveI : FiniteDimensional F E'⟮x⟯ := FiniteDimensional.trans F E' E'⟮x⟯
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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⟯
⊢ IsSeparable F x
have this₁ : 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⟯
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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⟯
⊢ IsSeparable F x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (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 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⟯
⊢ IsSeparable F x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x, y⟯
have rw : Algebra.IsSeparable.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)
Tactic: rw [← adjoin_simple_adjoin_simple]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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
⊢ Algebra.IsSeparable.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)
have hy₁ : IsSeparable (↥F⟮x⟯) y
Tactic: replace hy := IsSeparable.tower_top F⟮x⟯ hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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 ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)
have hx₁ : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
Tactic: rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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.{u, v} F ↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)
have hy₁ : Algebra.IsSeparable.{v, v} ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
Tactic: rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
have refine_1 : PerfectField F → ∀ (f : F[X]) (hf : f.natSepDegree = 1) (h : ∀ {f : F[X]}, Irreducible f → f.Separable), f.Splits
Tactic: refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
refine_1 :
  PerfectField F → ∀ (f : F[X]) (hf : f.natSepDegree = 1) (h : ∀ {f : F[X]}, Irreducible f → f.Separable), f.Splits
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
have refine_2 : ∀ (h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits), PerfectField F
Tactic: refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
⊢ f.Splits
have hf0 : f ≠ 0
Tactic: have hf0 : f ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
⊢ f.Splits
have refine_1 : ∀ (u : F[X]ˣ) (hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f), f.Splits
Tactic: obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hf0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
⊢ f.Splits
have refine_1 : ((UniqueFactorizationMonoid.factors f).prod * (↑u : F[X])).Splits
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
⊢ ((UniqueFactorizationMonoid.factors f).prod * (↑u : F[X])).Splits
have refine_1 : ∀ (g : F[X]) (hg : g ∈ UniqueFactorizationMonoid.factors f), g.Splits
Tactic: refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
⊢ g.Splits
have h₁ : g.Separable
Tactic: specialize h (UniqueFactorizationMonoid.irreducible_of_factor g hg)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
⊢ g.Splits
have key : g.natSepDegree ≤ f.natSepDegree
Tactic: have key := natSepDegree_le_of_dvd g f (UniqueFactorizationMonoid.dvd_of_mem_factors hg) hf0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
h_1 : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * (↑u : F[X]) = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
h : g.Separable
key : g.natSepDegree ≤ f.natSepDegree
⊢ g.Splits
have key₁ : g.natDegree ≤ 1
Tactic: rw [h.natSepDegree_eq_natDegree, hf] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
⊢ PerfectField F
have refine_2 : ∀ (p : ℕ), ExpChar F p → PerfectField F
Tactic: obtain ⟨p, _⟩ := ExpChar.exists F
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x : F
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x
have obtain : ∀ (y : F) (hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0),
  ∃ (a : F), (frobenius F p : (a : F) → F) a = x
Tactic: obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'