mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ LieRing.IsNilpotent L

pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range

Tactic:
·

Goal state after:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent ↥(ad R L).range
⊢ LieRing.IsNilpotent L
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range

Tactic:
·

Goal state after:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieRing.IsNilpotent L → LieRing.IsNilpotent ↥(ad R L).range
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L

pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ f = 1 ∨ g = 1

pp: case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1

Tactic:
·

Goal state after:
case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ f = 1 ∨ g = 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1

Tactic:
·

Goal state after:
case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊤.FG → Algebra.EssFiniteType F E

pp: case mpr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Algebra.EssFiniteType F E → ⊤.FG

Tactic:
·

Goal state after:
case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊤.FG → Algebra.EssFiniteType F E
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro.left
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

pp: case intro.right
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
·

Goal state after:
case intro.left
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro.right
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
·

Goal state after:
case intro.right
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro.right.a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)

pp: case a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Tactic:
·

Goal state after:
case intro.right.a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case mpr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Algebra.EssFiniteType F E → ⊤.FG

Tactic:
·

Goal state after:
case mpr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Algebra.EssFiniteType F E → ⊤.FG
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Tactic:
·

Goal state after:
case a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂

Goal state after:
case h
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
⊢ (∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a) → ⟦g₁⟧ = ⟦g₂⟧
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : Module.Finite R ↥A ∧ Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

pp: case neg
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
·

Goal state after:
case pos
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : Module.Finite R ↥A ∧ Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (Polynomial.map (algebraMap F L) (f * g)).Splits

pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
·

Goal state after:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (Polynomial.map (algebraMap F L) (f * g)).Splits
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : ¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
·

Goal state after:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
·

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)

pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑(insert a s)) →ₐ[F] L)

Tactic:
·

Goal state after:
case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ (Polynomial.map (algebraMap K L) p).Splits

pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤

Tactic:
·

Goal state after:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ (Polynomial.map (algebraMap K L) p).Splits
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤

Tactic:
·

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤
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:
simpa only [add_comm] using minpoly_add_algebraMap_splits r g

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

Goal state before:
pp: case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap (↥(adjoin F S)) E) ⊆ ↑(adjoin F (S ∪ T))

pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))

pp: case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)

pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
·

Goal state after:
case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap (↥(adjoin F S)) E) ⊆ ↑(adjoin F (S ∪ T))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))

pp: case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)

pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
·

Goal state after:
case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ T ⊆ ↑(adjoin F (S ∪ T))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)

pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
·

Goal state after:
case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
·

Goal state after:
case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case refine_1
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 ↑∅)

pp: case refine_2
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⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F ↑(insert x✝³ x✝²))

Tactic:
·

Goal state after:
case refine_1
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 ↑∅)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case refine_2
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⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F ↑(insert x✝³ x✝²))

Tactic:
·

Goal state after:
case refine_2
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⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F ↑(insert x✝³ x✝²))
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

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

Tactic:
obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

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

pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
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✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : p.degree ≤ 0
⊢ p = C (p.coeff 0)
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
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✝ : IsAlgClosed k
p : k[X]
h : p.roots = 0
hd : 0 < p.degree
⊢ p = C (p.coeff 0)
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

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

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

Tactic:
·

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

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
⊢ ¬(p = 0 ∧ q = 0)

pp: case refine_2
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
⊢ x ∣ p → ¬x ∣ q

Tactic:
·

Goal state after:
case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0
⊢ ¬(p = 0 ∧ q = 0)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ adjoin L ↑s ≤ E'

pp: case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ E' ≤ adjoin L ↑s

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ adjoin L ↑s ≤ E'