mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ (fun x_1 ↦ x * x_1 * x⁻¹) ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z ∈ {{1}}, z ⊆ x ∩ y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → 1 ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V * V ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = B.filter

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
g : F[X]
h1 : g.Separable
n : ℕ
hm : ((expand F (q ^ n)) g).Monic
hi : Irreducible ((expand F (q ^ n)) g)
h : ((expand F (q ^ n)) g).natSepDegree = 1
h2 : g.natDegree = 1
⊢ (expand F (q ^ n)) (X + C (g.coeff 0)) = (expand F (q ^ n)) (X - C (-g.coeff 0))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = B.N x₀

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ 𝓝 1 = B.filter

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = (expand F (q ^ n)) (X - C y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ (𝓝 1).HasBasis (fun V ↦ V ∈ B) id

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = X ^ q ^ n - C y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ U ∈ 𝓝 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this✝ : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
this : ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B, ∃ ia, (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ IsTopologicalGroup G

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits
⊢ Nat.card Gal(↥F⟮α⟯/F) = finrank F ↥F⟮α⟯

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ F⟮α⟯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ T2Space G ↔ ⋂₀ F.sets = {1}

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e ↦ ↑e, invFun := fun e ↦ ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F E) (minpoly F α)).Splits
⊢ (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ T2Space G ↔ ⋂₀ F.sets ⊆ {1}

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Nat.card Gal(E/F) = finrank F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝¹ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this✝ : IsTopologicalAddGroup R
this : ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B', ∃ ia, (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
⊢ FiniteDimensional F E

Tactic:
by

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

Goal state before:
pp: F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
x : E
⊢ x ∈ fixedField H ↔ ∀ f ∈ H, f x = x

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ fixedField ⊥ = ⊤

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup Gal(E/F)
inst✝ : FiniteDimensional F E
⊢ finrank (↥(fixedField H)) E = Nat.card ↥H

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊤.fixingSubgroup = ⊥

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊥.fixingSubgroup = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
⊢ f.natSepDegree = 1 ↔ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
h' : ¬IsIntegral F x
⊢ False

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K L : IntermediateField F E
φ : Gal(E/F)
⊢ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup → φ ∈ (K ⊔ L).fixingSubgroup

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x✝¹ x✝ : ↥K.fixingSubgroup
⊢ (let __src := (↑(x✝¹ * x✝)).toRingEquiv;
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) =
    (let __src := (↑x✝¹).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) *
      let __src := (↑x✝).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup Gal(E/F)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
this : Nat.card ↥H = Nat.card ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup Gal(E/F)
inst✝ : FiniteDimensional F E
⊢ (fixedField H).fixingSubgroup = H

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ϕ • (↑x * ↑y) = ↑x * ↑y

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ separableClosure F K ↔ x ∈ separableClosure F E

Tactic:
by

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

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
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
this : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (separableClosure F K) = separableClosure F E

Tactic:
by

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

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
inst✝ : FiniteDimensional F E
h : IsGalois F E
⊢ fixedField K.fixingSubgroup = K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ fixedField ⊤ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ separableClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
x : ↥(separableClosure F E)
⊢ IsSeparable F x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsSeparable F x
x : E
h : x ∈ L
⊢ x ∈ separableClosure F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F E

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
x : E
⊢ x ∈ ⊥ ↔ ∀ (f : Gal(E/F)), f x = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
⊢ IsTopologicalRing R

Tactic:
by

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

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
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Nat.card ↥K.fixingSubgroup = finrank (↥K) E

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃ V ∈ 𝓝 0,
        ∃
          W ∈
            (have this := default;
              this).sets,
          V • W ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
L1 L2 : IntermediateField F E
h1 : Algebra.IsSeparable F ↥L1
h2 : Algebra.IsSeparable F ↥L2
⊢ Algebra.IsSeparable F ↥(L1 ⊔ L2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃
        V ∈
          (have this := default;
            this).sets,
        V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable F ↥(t i)
⊢ Algebra.IsSeparable F ↥(⨆ i, t i)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        L ↔
    K ≤ L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ (m₀ : M) {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ (m₀ : M) {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
by
        rintro m₀ U (h : U ∈ (0 : Set (Set M)))
        rw [Set.mem_zero] at h
        simp [h, nhds_discrete]

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K : IntermediateField F E
H : Subgroup Gal(E/F)
⊢ fixedField H = K ↔ K.fixingSubgroup = H

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : Normal K ↥E
⊢ (restrictNormalHom ↥E).ker = E.fixingSubgroup

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ ClosureOperator (IntermediateField F E)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ (separableClosureOperator F E) (IntermediateField.restrictScalars F (separableClosure K E))
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure K E)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E✝ : Type u_2
inst✝⁵ : Field E✝
inst✝⁴ : Algebra F E✝
H✝ : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
⊢ Normal K ↥(fixedField H)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
⊢ finInsepDegree F E = finInsepDegree F K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ sepDegree F F = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ insepDegree F F = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ finInsepDegree F F = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ : Gal(L/K)
⊢ (map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
E✝ : Type u_2
inst✝⁶ : Field E✝
inst✝⁵ : Algebra F E✝
H : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
⊢ E.fixingSubgroup.Normal

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin F ↑s)) E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty

Tactic:
by

Goal state after: