mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : Subfield E
HF : Set.range ⇑(algebraMap F E) ⊆ ↑K
HS : S ⊆ ↑K
⊢ (adjoin F S).toSubfield ≤ K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) ((minpoly K x).comp (-X))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K (-x))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K (x + (algebraMap K L) r))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K (x - (algebraMap K L) r))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K ((algebraMap K L) r + x))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K ((algebraMap K L) r - x))).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing M
inst✝³ : Algebra R K
inst✝² : Algebra R M
inst✝¹ : Algebra K M
inst✝ : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R L) (minpoly R x)).Splits
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = adjoin F (S ∪ T)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommSemiring F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommSemiring E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : Algebra K E
inst✝ : IsScalarTower K F E
⊢ adjoin F ↑(adjoin K S) = adjoin F S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
⊢ adjoin F (insert x ↑(adjoin F S)) = adjoin F (insert x S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
α : ↥K
⊢ lift (adjoin F {α}) = adjoin F {↑α}

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ lift ⊤ = K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
L L' : IntermediateField F ↥K
⊢ lift (L ⊔ L') = lift L ⊔ lift L'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
L L' : IntermediateField F ↥K
⊢ lift (L ⊓ L') = lift L ⊓ lift L'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ restrictScalars F (extendScalars h) = restrictScalars F (adjoin (↥K) S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = K ⊔ adjoin F S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_3
f : ι → IntermediateField F E
⊢ ⨆ i, f i = adjoin F (⋃ i, ↑(f i))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝¹⁰ : Field F
E : Type u_2
inst✝⁹ : Field E
inst✝⁸ : Algebra F E
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
⊢ K = K'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝¹⁰ : Field F
E : Type u_2
inst✝⁹ : Field E
inst✝⁸ : Algebra F E
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ restrictScalars F (adjoin L S) = restrictScalars F (adjoin L' S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x : E
h : x ∈ adjoin F s
⊢ p 1 ⋯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x✝¹ : E
h✝ : x✝¹ ∈ adjoin F s
x : E
x✝ : x ∈ Subfield.closure (Set.range ⇑(Algebra.algebraMap F E) ∪ s)
h : p x x✝
⊢ p (-x) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₂ ⟨x✝³ + x✝², ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
S : IntermediateField F E
s : Set E
hS : S = adjoin F s
φ₁ φ₂ : ↥S →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
K : IntermediateField F E
⊢ F⟮α⟯ ≤ K ↔ α ∈ K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ ⨆ x ∈ S, F⟮x⟯ = adjoin F S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝⁹ : Field F
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈ A⟮(algebraMap B C) b⟯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ adjoin F S = ⊥ ↔ S ⊆ ↑⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ F⟮α⟯ = ⊥ ↔ α ∈ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℤ
⊢ F⟮↑n⟯ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ adjoin F ↑∅ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
hS : S.FG
hT : T.FG
⊢ (S ⊔ T).FG

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
h : ∀ (i : ι), (S i).FG
⊢ (⨆ i, S i).FG

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ Field.FG F ↔ ⊤.FG

Tactic:
simp [Field.fg_iff, fg_def, Set.exists_finite_iff_finset,
    ← toSubfield_inj, Subfield.algebraMap_ofSubfield, Subfield.closure_union]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ Field.FG F ↔ ⊤.FG

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
⊢ P (adjoin F ↑S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)
K : IntermediateField F E
hK : K.FG
⊢ P K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L'
h : S ≤ f.fieldRange
⊢ map f (comap f S) = S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: L : Type u_2
inst✝ : Field L
F : Subfield L
⊢ extendScalars ⋯ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: L : Type u_2
inst✝ : Field L
F : Subfield L
⊢ (extendScalars ⋯).toSubfield = ⊤.toSubfield

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: K : Type u_1
inst✝² : Field K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
⊢ restrictScalars K (extendScalars ⋯) = restrictScalars K ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: K : Type u_1
inst✝² : Field K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
⊢ restrictScalars K (extendScalars ⋯) = restrictScalars K ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ r ∈ σ a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
⊢ q.IsRoot k

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
⊢ ↑ₐ (eval k p) - (aeval a) p = (aeval a) q

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
⊢ (fun x ↦ eval x p) '' σ a ⊆ σ ((aeval a) p)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ σ ((aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
⊢ ?m.75 < (C k - p).degree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : Lifts F E K
⊢ ∀ (x : ↥L.carrier), L.emb ((inclusion ⋯) x) = L.emb x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ (X ^ n - C x).degree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ σ ((aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
⊢ (aeval a) (C k - p) = ↑ₐ k - (aeval a) p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
⊢ ∃ z, x = z * z

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
hp : p = C (p.coeff 0)
⊢ p.roots = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L₁ L₂ L₃ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h) x) = L₁.emb x) →
    (∃ (h : L₂.carrier ≤ L₃.carrier), ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h) x) = L₂.emb x) →
      ∃ (h : L₁.carrier ≤ L₃.carrier), ∀ (x : ↥L₁.carrier), L₃.emb ((inclusion h) x) = L₁.emb x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
⊢ p.roots = 0 ↔ p = C (p.coeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
⊢ p.roots.card = p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
⊢ (map f p).degree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
x : k
hx : (map f p).IsRoot x
⊢ eval₂ f x p = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ eval x p = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
⊢ ∀ (a b : Lifts F E K),
    (∃ (h : a.carrier ≤ b.carrier), ∀ (x : ↥a.carrier), b.emb ((inclusion h) x) = a.emb x) →
      (∃ (h : b.carrier ≤ a.carrier), ∀ (x : ↥b.carrier), a.emb ((inclusion h) x) = b.emb x) → a = b

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : Lifts F E K
x : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(botEquiv F E) }.carrier
⊢ L.emb ((inclusion ⋯) x) = { carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(botEquiv F E) }.emb x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
⊢ IsAlgClosed k

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ (map e.symm.toRingHom p).degree ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (C k - p) = 0
⊢ k = (fun x ↦ eval x p) r

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
⊢ σ ((aeval a) p) = (fun x ↦ eval x p) '' σ a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
⊢ σ ((aeval a) p) = (fun k ↦ eval k p) '' σ a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun x ↦ x ^ n) '' σ a ⊆ σ (a ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < (X ^ n).degree

Tactic:
by

Goal state after: