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

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ ∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣ Polynomial.map (subfield G F).subtype f

Tactic:
]

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ ∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣ Polynomial.map (subfield G F).subtype f
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂)) (((AlgEquiv.restrictNormalHom K₁) f) x) =
    ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂))
      ((((AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)) f) x)

Tactic:
]

Goal state after:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂)) (((AlgEquiv.restrictNormalHom K₁) f) x) =
    ((algebraMap K₂ K₃).comp (algebraMap K₁ K₂))
      ((((AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)) f) x)
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: K₁ : Type u_6
K₂ : Type u_7
F : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
⊢ (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f) =
    (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: 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
⊢ f ∣ f * g

Tactic:
]

Goal state after:
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
⊢ f ∣ f * g
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: 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
⊢ g ∣ f * g

Tactic:
]

Goal state after:
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
⊢ g ∣ f * g
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: 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 ∨ Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1

Tactic:
]

Goal state after:
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 ∨ Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1
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 : g = 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
hf3 : f = minpoly G F x
⊢ 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 : g = 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
hf3 : f = minpoly G F x
⊢ 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 = 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 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 = 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g))).Splits

Tactic:
]

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g))).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (prodXSubSMul G F x).Separable

Tactic:
]

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (prodXSubSMul G F x).Separable
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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 : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ Algebra.adjoin F S = (adjoin F S).toSubalgebra

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ Algebra.adjoin F S = (adjoin F S).toSubalgebra
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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 : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ Module.rank (↥(subfield G F)) F ≤ ↑(Fintype.card G)

Tactic:
]

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ Module.rank (↥(subfield G F)) F ≤ ↑(Fintype.card G)
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
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) ∧
    Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
]

Goal state after:
case intro
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) ∧
    Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)
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
s : Finset E
hs : adjoin F ↑s = ⊤
this✝¹ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this✝ : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
this : Algebra.EssFiniteType F ↥⊤
⊢ Algebra.EssFiniteType F E

Tactic:
]

Goal state after:
case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Finset E
hs : adjoin F ↑s = ⊤
this✝¹ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this✝ : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
this : Algebra.EssFiniteType F ↥⊤
⊢ Algebra.EssFiniteType F E
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) ≤ finrank (↥(subfield G F)) F

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) ≤ finrank (↥(subfield G F)) F
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
x✝ : IsLocalization.mk' E x s ∈ ⊤
hs : ↑↑s ≠ 0
H : IsLocalization.mk' E x s = ↑x / ↑↑s
⊢ ↑x / ↑↑s ∈ adjoin F ↑(Algebra.EssFiniteType.finset F E)

Tactic:
]

Goal state after:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
x✝ : IsLocalization.mk' E x s ∈ ⊤
hs : ↑↑s ≠ 0
H : IsLocalization.mk' E x s = ↑x / ↑↑s
⊢ ↑x / ↑↑s ∈ adjoin F ↑(Algebra.EssFiniteType.finset F E)
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case refine_1
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
x✝¹ x✝ : G
h :
  ∀ (x : F),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝¹) x =
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝) x
⊢ ∀ (x : F),
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝¹) x = (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝) x

Tactic:
]

Goal state after:
case refine_1
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
x✝¹ x✝ : G
h :
  ∀ (x : F),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝¹) x =
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝) x
⊢ ∀ (x : F),
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝¹) x = (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝) x
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case refine_2
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
f : Gal(F/↥(subfield G F))
x✝ : G
h : ∀ (x : F), (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝) x = ↑f x
⊢ ∀ (x : F), ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝) x = f x

Tactic:
]

Goal state after:
case refine_2
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
f : Gal(F/↥(subfield G F))
x✝ : G
h : ∀ (x : F), (MulSemiringAction.toAlgHom (↥(subfield G F)) F x✝) x = ↑f x
⊢ ∀ (x : F), ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) x✝) x = f x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
⊢ Algebra.EssFiniteType F E

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
⊢ Algebra.EssFiniteType F E
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F (gen F α)

Tactic:
]

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

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
hS : ∀ x ∈ S, IsAlgebraic F x
⊢ (adjoin F S).toSubalgebra = ⊤ ↔ (adjoin F S).toSubalgebra = ⊤

Tactic:
]

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

Goal state before:
pp: case h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ (adjoin F ↑s).toSubalgebra = ⊤

Tactic:
]

Goal state after:
case h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ (adjoin F ↑s).toSubalgebra = ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
]

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: 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
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ ∀ (a : F), (f g₁) a = (f g₂) a

Tactic:
]

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
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ ∀ (a : F), (f g₁) a = (f g₂) a
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
]

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra

Tactic:
]

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
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✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
g : G
hg : ∀ (a : F), ((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) ↑g) a = (AlgEquiv.ofRingEquiv ⋯) a
⊢ ∀ (a : F), ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) g) a = f a

Tactic:
]

Goal state after:
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✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
g : G
hg : ∀ (a : F), ((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) ↑g) a = (AlgEquiv.ofRingEquiv ⋯) a
⊢ ∀ (a : F), ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F) g) a = f a
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin ↥E' ↑L)

Tactic:
]

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin ↥E' ↑L)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Algebra.adjoin F (↑E'.toSubalgebra ∪ ↑L)

Tactic:
]

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (adjoin F (↑E' ∪ ↑L)).toSubalgebra = Algebra.adjoin F (↑E'.toSubalgebra ∪ ↑L)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring

Tactic:
]

Goal state after:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: 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
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i ↦ ↑(bA i)) * Set.range fun i ↦ ↑(bB i))
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
]

Goal state after:
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
ιA : Type v
bA : Basis ιA R ↥A
ιB : Type v
bB : Basis ιB R ↥B
h : toSubmodule (A ⊔ B) = Submodule.span R ((Set.range fun i ↦ ↑(bA i)) * Set.range fun i ↦ ↑(bB i))
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: 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 : F[X]
inst✝ : IsSplittingField F L f
⊢ (Polynomial.map (algebraMap F L) f).Splits

Tactic:
]

Goal state after:
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 : F[X]
inst✝ : IsSplittingField F L f
⊢ (Polynomial.map (algebraMap F L) f).Splits