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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
x✝ : ι
⊢ (Subtype.val ∘ fun i ↦ ⟨x i, ⋯⟩) x✝ = x x✝

Tactic:
;

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
x✝ : ι
⊢ (Subtype.val ∘ fun i ↦ ⟨x i, ⋯⟩) x✝ = x x✝
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ g • h⁻¹ • x = h⁻¹ • x ↔ x ∈ fixedBy α g

Tactic:
← mul_smul,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Rv ≤ (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R (range v)

Tactic:
;

Goal state after:
R : Type u_1
S : Type v
A : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Rv ≤ (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R (range v)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nonempty ι
a✝ : Nontrivial R
⊢ IsTranscendenceBasis R X

Tactic:
;

Goal state after:
ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nonempty ι
a✝ : Nontrivial R
⊢ IsTranscendenceBasis R X
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case e'_7
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
x✝ : PUnit.{1}
m✝ : PUnit.{1} →₀ ℕ
⊢ coeff m✝ ((⇑(uniqueAlgEquiv R PUnit.{1}).symm ∘ (fun x ↦ Polynomial.X) ∘ ⇑(Equiv.equivPUnit ι).symm) x✝) =
    coeff m✝ (X x✝)

Tactic:
;

Goal state after:
case e'_7
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
x✝ : PUnit.{1}
m✝ : PUnit.{1} →₀ ℕ
⊢ coeff m✝ ((⇑(uniqueAlgEquiv R PUnit.{1}).symm ∘ (fun x ↦ Polynomial.X) ∘ ⇑(Equiv.equivPUnit ι).symm) x✝) =
    coeff m✝ (X x✝)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : Nonempty ι
hy : IsTranscendenceBasis S y
h✝ : Subsingleton R
⊢ Nonempty (ι' ⊕ ι)

Tactic:
;

Goal state after:
case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : Nonempty ι
hy : IsTranscendenceBasis S y
h✝ : Subsingleton R
⊢ Nonempty (ι' ⊕ ι)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
⊢ Algebra ↥Rxy ↥Sy

Tactic:
refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
⊢ range y ⊆ ↑(Subalgebra.restrictScalars (↥Rx) Sy)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
i : ι'
⊢ y i ∈ ↑(Subalgebra.restrictScalars (↥Rx) Sy)

Tactic:
;

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
i : ι'
⊢ y i ∈ ↑(Subalgebra.restrictScalars (↥Rx) Sy)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝¹ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝ : ↥Sy
a : A
ha : a ∈ Sy
i : ι'
⊢ IsAlgebraic ↥Rxy ⟨y i, ⋯⟩

Tactic:
;

Goal state after:
case refine_1
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝¹ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝ : ↥Sy
a : A
ha : a ∈ Sy
i : ι'
⊢ IsAlgebraic ↥Rxy ⟨y i, ⋯⟩
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ Nonempty ι ↔ Algebra.Transcendental R A

Tactic:
← not_isEmpty_iff,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ ¬IsEmpty ι ↔ Algebra.Transcendental R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
B : Set A
⊢ Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B

Tactic:
;

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
B : Set A
⊢ Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R s)) (_root_.id a)

Tactic:
;

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R s)) (_root_.id a)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ ↑S

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ ↑S
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : F
⊢ ((algebraMap F E).comp ↑(RingEquiv.refl F)) x✝ = ((↑topEquiv.toRingEquiv).comp (algebraMap F ↥⊤)) x✝

Tactic:
;

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : F
⊢ ((algebraMap F E).comp ↑(RingEquiv.refl F)) x✝ = ((↑topEquiv.toRingEquiv).comp (algebraMap F ↥⊤)) x✝
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ trdeg R S + trdeg S A = trdeg R A

Tactic:
rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]

Goal state after:
R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)
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
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this✝ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this : Nontrivial S
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
have := (isDomain_iff_noZeroDivisors_and_nontrivial S).mpr ⟨‹_›, ‹_›⟩

Goal state after:
ι : 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
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this✝¹ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝ : Nontrivial S
this : IsDomain S
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl.refl
ι : 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
s : Set ι
i : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : i ∈ insert i s
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {i})))
H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))
hj' : i ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
;

Goal state after:
case inl.refl
ι : 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
s : Set ι
i : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : i ∈ insert i s
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {i})))
H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))
hj' : i ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
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, f = (expand F (q ^ n)) (X - C y)

Tactic:
obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q

Goal state after:
case refine_1
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
⊢ ∃ n_1 y, (expand F (q ^ n)) g = (expand F (q ^ n_1)) (X - C y)
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 ⊆ U

Tactic:
;

Goal state after:
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 ⊆ U
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hi : Irreducible ((X ^ q ^ n.pred) ^ q - C z ^ q)
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Tactic:
← sub_pow_expChar

Goal state after:
case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hi : Irreducible ((X ^ q ^ n.pred - C z) ^ q)
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False
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
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
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
have hF := finiteMultiplicity_of_degree_pos_of_monic (degree_pos_of_irreducible hI) hM hm.ne_zero

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
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
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
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 ∈ ⊤

Tactic:
;

Goal state after:
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 ∈ ⊤
Module: Mathlib.FieldTheory.Galois.Basic

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

Tactic:
;

Goal state after:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois F E
⊢ IsGalois (↥⊥) E
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:
refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩
  · obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h
    exact ⟨m, n, y, hm, h⟩
  simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]

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
a✝ : E
⊢ (let __src := (↑(x✝¹ * x✝)).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝ =
    ((let __src := (↑x✝¹).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) *
        let __src := (↑x✝).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝

Tactic:
;

Goal state after:
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
a✝ : E
⊢ (let __src := (↑(x✝¹ * x✝)).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝ =
    ((let __src := (↑x✝¹).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) *
        let __src := (↑x✝).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_1
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
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

pp: case convert_2.refine_2
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
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
⊢ (minpoly F x).natSepDegree = 1

Tactic:
· obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    exact ⟨n, y, hx ▸ aeval F x⟩

Goal state after:
case convert_2.refine_2
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
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
⊢ (minpoly F x).natSepDegree = 1
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
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Set E
ht : (fun t ↦ IsTranscendenceBasis F Subtype.val) t
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) t
⊢ False

Tactic:
have : t.Finite := by
    simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.natCast_lt_aleph0]

Goal state after:
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
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Set E
ht : (fun t ↦ IsTranscendenceBasis F Subtype.val) t
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) t
this : t.Finite
⊢ False
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
s : Set K
inst✝ : Finite ↑s
⊢ (adjoin k (⇑f '' s)).toIntermediateField = (adjoin k s).toIntermediateField

Tactic:
;

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
s : Set K
inst✝ : Finite ↑s
⊢ (adjoin k (⇑f '' s)).toIntermediateField = (adjoin k s).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:
(Tactic.tacticSeq1Indented
 [(Tactic.simpa
   "simpa"
   []
   []
   (Tactic.simpaArgsRest
    (Tactic.optConfig [])
    []
    ["only"]
    [(Tactic.simpArgs "[" [(Tactic.simpLemma [] [] `Set.image_singleton)] "]")]
    ["using"
     (Term.app
      `adjoin_map
      [`f
       (choice
        («term{_}» "{" [`x] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
         (Term.optEllipsis [])
         []
         "}"))])]))])

Goal state after: