mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ IsIntegral K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ IsIntegral K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ IsUnit (?x * p)

pp: case x
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ K[X]

Tactic:
rw [← hc, (integerNormalization R⁰ p).eq_C_content_mul_primPart, ← hu, ← map_mul, isUnit_iff]

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ ∃ r, IsUnit r ∧ C r = map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a.ind.refine_1
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)

pp: case a.ind.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree

Tactic:
·

Goal state after:
case a.ind.refine_1
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a.ind.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree

Tactic:
·

Goal state after:
case a.ind.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu.inl
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : p = 0
⊢ False

pp: case hu.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : ↑u = 0
⊢ False

Tactic:
·

Goal state after:
case hu.inl
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : p = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : ↑u = 0
⊢ False

Tactic:
·

Goal state after:
case hu.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : ↑u = 0
⊢ False
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
by_cases hx : IsIntegral R x

Goal state after:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
·

Goal state after:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
·

Goal state after:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ ∀ (i : L →ₐ[K] E),
    eval (i x) (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0

pp: case hcard
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)

Tactic:
·

Goal state after:
case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ ∀ (i : L →ₐ[K] E),
    eval (i x) (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : a = 0
⊢ f.natDegree ≠ 0

pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : ¬a = 0
⊢ f.natDegree ≠ 0

Tactic:
·

Goal state after:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : a = 0
⊢ f.natDegree ≠ 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : ¬a = 0
⊢ f.natDegree ≠ 0

Tactic:
·

Goal state after:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : ¬a = 0
⊢ f.natDegree ≠ 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ f.natDegree ≠ 0

Tactic:
by
    have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind
    by_cases ha : a = 0
    · grind [zero_add]
    · grind [natDegree_add_eq_left_of_natDegree_lt]

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : x = 0
⊢ ∃ z, z ^ n = x

pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x

Tactic:
·

Goal state after:
case pos
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : x = 0
⊢ ∃ z, z ^ n = x
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x

Tactic:
·

Goal state after:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)

pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Tactic:
·

Goal state after:
case inl
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case hcard
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)

Tactic:
·

Goal state after:
case hcard
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)

Tactic:
·

Goal state after:
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ Finset.fold max 0 (natDegree ∘ fun σ ↦ map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x))
      Finset.univ <
    Fintype.card (L →ₐ[K] E)

pp: case hcard.refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ (X ^ r).natDegree < Fintype.card (L →ₐ[K] E)

Tactic:
·

Goal state after:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ Finset.fold max 0 (natDegree ∘ fun σ ↦ map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x))
      Finset.univ <
    Fintype.card (L →ₐ[K] E)
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case pos
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : p = 0
⊢ p.Splits

pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
⊢ p.Splits

Tactic:
·

Goal state after:
case pos
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : p = 0
⊢ p.Splits