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

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : MvPolynomial.X i ^ (m + 1) = MvPolynomial.X i ^ (n + 1)
⊢ m = n

Tactic:
simpa using

Goal state after:
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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : MvPolynomial.X i ^ (m + 1) = MvPolynomial.X i ^ (n + 1)
⊢ m = n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ Fintype.card ↥(f.aroots f.SplittingField).toFinset = f.natDegree

Tactic:
Fintype.card_coe

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
simpa using

Goal state after:
case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) f = 0

Tactic:
simpa using

Goal state after:
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) f = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) g = 0

Tactic:
simpa using

Goal state after:
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) g = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False

Tactic:
simpa using

Goal state after:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
simpa using

Goal state after:
case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand (AlgebraicClosure F) (q ^ n)) (map (algebraMap F (AlgebraicClosure F)) f)).roots.toFinset.card =
    (map (algebraMap F (AlgebraicClosure F)) f).roots.toFinset.card
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
⊢ U ∈ B.toFilterBasis → a ∈ (fun y ↦ a * y) '' id U

Tactic:
U_in

Goal state after:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
⊢ a ∈ (fun y ↦ a * y) '' id U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
⊢ U ∈ B.toFilterBasis →
    ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id U ∈ map (fun y ↦ x * y) B.filter

Tactic:
U_in

Goal state after:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
⊢ ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id U ∈ map (fun y ↦ x * y) B.filter
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
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
U : Set G
⊢ U ∈ B → ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
U_in

Goal state after:
case refine_1
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
U : Set G
U_in : U ∈ B
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
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
U : Set G
⊢ U ∈ B → ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U

Tactic:
U_in

Goal state after:
case refine_2
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
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_4
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
x₀ : G
U : Set G
⊢ U ∈ B → ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id U

Tactic:
U_in

Goal state after:
case refine_4
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
x₀ : G
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id U
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
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
simpa using

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = p ^ multiplicity p f
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul
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
U : Set R
⊢ U ∈ B' → ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
U_in

Goal state after:
case hmul
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
U : Set R
U_in : U ∈ B'
⊢ ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
U : Set M
⊢ U ∈ BM.sets → ∃ V ∈ 𝓝 0, ∃ W ∈ BM.sets, V • W ⊆ U

Tactic:
U_in

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
U : Set M
U_in : U ∈ BM.sets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ BM.sets, V • W ⊆ U
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : ∃ T ∈ 𝓝 1, U * T ⊆ W
x✝ : ∃ T ∈ 𝓝 1, V * T ⊆ W
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ (U ∪ V) * (T₁ ∩ T₂) ⊆ W

Tactic:
rw [union_mul]

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : ∃ T ∈ 𝓝 1, U * T ⊆ W
x✝ : ∃ T ∈ 𝓝 1, V * T ⊆ W
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
⊢ U ∈ BM.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
U_in

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in : U ∈ BM.sets
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝⁻¹ ∈ V⁻¹ ^ (k + 1)

Tactic:
simpa using

Goal state after:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝ ∈ V ^ (k + 1)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
L : IntermediateField F E
inst✝ : Algebra.IsSeparable F ↥L
x : E
h : x ∈ L
⊢ IsSeparable F x

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
L : IntermediateField F E
inst✝ : Algebra.IsSeparable F ↥L
x : E
h : x ∈ L
⊢ (minpoly F x).Separable
Module: Mathlib.FieldTheory.SeparableDegree

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
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
⊢ (aeval x) g = 0

Tactic:
simpa using

Goal state after:
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
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
⊢ (aeval x) g = 0
Module: Mathlib.FieldTheory.Galois.GaloisClosure

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
toIntermediateField✝¹ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥toIntermediateField✝¹
isGalois✝¹ : IsGalois k ↥toIntermediateField✝¹
toIntermediateField✝ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥toIntermediateField✝
isGalois✝ : IsGalois k ↥toIntermediateField✝
eq :
  { toIntermediateField := toIntermediateField✝¹, finiteDimensional := finiteDimensional✝¹,
        isGalois := isGalois✝¹ }.toIntermediateField =
    { toIntermediateField := toIntermediateField✝, finiteDimensional := finiteDimensional✝,
        isGalois := isGalois✝ }.toIntermediateField
⊢ { toIntermediateField := toIntermediateField✝¹, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } =
    { toIntermediateField := toIntermediateField✝, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }

Tactic:
simpa using

Goal state after:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
toIntermediateField✝¹ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥toIntermediateField✝¹
isGalois✝¹ : IsGalois k ↥toIntermediateField✝¹
toIntermediateField✝ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥toIntermediateField✝
isGalois✝ : IsGalois k ↥toIntermediateField✝
eq :
  { toIntermediateField := toIntermediateField✝¹, finiteDimensional := finiteDimensional✝¹,
        isGalois := isGalois✝¹ }.toIntermediateField =
    { toIntermediateField := toIntermediateField✝, finiteDimensional := finiteDimensional✝,
        isGalois := isGalois✝ }.toIntermediateField
⊢ toIntermediateField✝¹ = toIntermediateField✝
Module: Mathlib.FieldTheory.Galois.GaloisClosure

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
f : K →ₐ[k] K
x : K
⊢ adjoin k {f x} = adjoin k {x}

Tactic:
simpa using

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
f : K →ₐ[k] K
x : K
⊢ adjoin k {f x} = adjoin k {x}
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
g : Gal(L/K)
⊢ g ∈ MulAction.stabilizer Gal(L/K) x ↔ g ∈ E.fixingSubgroup

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
g : Gal(L/K)
⊢ g x = x ↔ ∀ x ∈ E, g x = x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
x : E
hx : x ∈ ↑L.toSubsemiring
h : (algebraMap E E') ((f.restrictNormal E) x) = (algebraMap E E') x
⊢ f (↑(IsScalarTower.toAlgHom F E E') x) = ↑(IsScalarTower.toAlgHom F E E') x

Tactic:
rwa [AlgEquiv.restrictNormal_commutes] at h

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'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
⊢ L ≤ E

Tactic:
simpa using

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
⊢ L ≤ E
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
a b : M
ha : a ∈ {x | ∀ y ∈ N, (B x) y ∈ 1}
hb : b ∈ {x | ∀ y ∈ N, (B x) y ∈ 1}
y : M
hy : y ∈ N
⊢ (B (a + b)) y ∈ 1

Tactic:
simpa using

Goal state after:
R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
a b : M
ha : a ∈ {x | ∀ y ∈ N, (B x) y ∈ 1}
hb : b ∈ {x | ∀ y ∈ N, (B x) y ∈ 1}
y : M
hy : y ∈ N
⊢ ∃ y_1, (algebraMap R S) y_1 = (B a) y + (B b) y
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
z : M
hz : z ∈ ↑N
⊢ (B ↑x) z = (B ↑y) z

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
z : M
hz : z ∈ ↑N
⊢ (B ↑x) z = (B ↑y) z
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ σ y (minpolyDiv R x * (X - C x)) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0

Tactic:
simpa using

Goal state after:
case neg
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ σ y (minpolyDiv R x * (X - C x)) = 0
h : ¬σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = 0
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ (Polynomial.aeval s) p = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ (Polynomial.aeval s) p = 0
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0

Tactic:
simpa using

Goal state after:
case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ (algebraMap R S) y (minpoly R x) = 0
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x : S
p : R[X]
hirr : Irreducible p
hp : (Polynomial.aeval x) p = 0
isUnit : IsUnit p.leadingCoeff
⊢ IsIntegral R x

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x : S
p : R[X]
hirr : Irreducible p
hp : (Polynomial.aeval x) p = 0
isUnit : IsUnit p.leadingCoeff
⊢ IsIntegral R x
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i ∈ R[x]

Tactic:
by_contra H
  have : ∀ j, coeff (minpolyDiv R x) (i + j) ∉ R[x] := by
    intro j; induction j with
    | zero => exact H
    | succ j IH =>
      intro H; apply IH
      rw [coeff_minpolyDiv]
      refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))
      exact Subalgebra.algebraMap_mem _ _
  apply this (natDegree (minpolyDiv R x) + 1)
  rw [coeff_eq_zero_of_natDegree_lt]
  · exact zero_mem _
  · lia

Goal state after: