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

Goal state before:
pp: k : Type u
inst✝²⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²⁵ : Field K
inst✝²⁴ : Field J
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Field L
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra R M
inst✝¹⁸ : IsTorsionFree R M
inst✝¹⁷ : IsAlgClosure R M
inst✝¹⁶ : Algebra K M
inst✝¹⁵ : IsAlgClosure K M
inst✝¹⁴ : Algebra S L
inst✝¹³ : IsTorsionFree S L
inst✝¹² : IsAlgClosure S L
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R L
inst✝⁹ : IsScalarTower R S L
inst✝⁸ : Algebra K J
inst✝⁷ : Algebra J L
inst✝⁶ : IsAlgClosure J L
inst✝⁵ : Algebra K L
inst✝⁴ : IsScalarTower K J L
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Algebra.IsAlgebraic R L
⊢ L ≃ₐ[R] M

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, (Polynomial.map (algebraMap K ↥(t i)) (p i)).Splits ∧ t i = adjoin K ((p i).rootSet L)
i : ι
hi : i ∈ s
⊢ (Polynomial.map (algebraMap K ↥(⨆ i ∈ s, t i)) (p i)).Splits

Tactic:
by

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

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝² : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝¹ : Algebra S R := hSR.toRingHom.toAlgebra
this✝ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this : IsScalarTower R S L
⊢ ∀ (x : S), (algebraMap S L) x = (algebraMap R L) ((algebraMap S R) x)

Tactic:
by

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : ∏ i ∈ s, p i ≠ 0
h : ∀ i ∈ s, IsSplittingField K (↥(t i)) (p i)
⊢ IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
by

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

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
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
this : ∀ (μ : K), m μ ∈ p
⊢ (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, p ⊓ (f.genEigenspace μ) k

Tactic:
by

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

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
⊢ { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Field L
inst✝⁸ : Field M
inst✝⁷ : Algebra R M
inst✝⁶ : IsTorsionFree R M
inst✝⁵ : IsAlgClosure R M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
r : R
⊢ (equivOfEquiv L M hSR) ((equivOfEquiv L M hSR).symm ((algebraMap R M) r)) =
    (equivOfEquiv L M hSR) ((algebraMap S L) (hSR.symm r))

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ IsCompactElement F⟮x⟯

Tactic:
by

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

Goal state before:
pp: k : Type u
inst✝⁶ : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field A
inst✝² : Algebra F K
inst✝¹ : Algebra F A
inst✝ : Algebra.IsAlgebraic F K
L : IntermediateField F A
hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits
f : K →ₐ[F] A
x : K
⊢ (Polynomial.map (algebraMap F ↥L) (minpoly F (f x))).Splits

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
⊢ IsCompactElement (adjoin F ↑S)

Tactic:
by

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

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
s : IntermediateField F E
⊢ ∀ x ∈ (fun x ↦ F⟮x⟯) '' ↑s, IsCompactElement x

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x✝ : E
hx : x✝ ∈ ⨆ i, f i
i : ι
x : E
h : x ∈ f i
⊢ F⟮x⟯ ≤ F⟮↑⟨i, ⟨x, h⟩⟩.snd⟯

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
⊢ ∃ τ ≥ union c hc, ↑S ⊆ ↑τ.carrier

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet E)

Tactic:
by

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

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
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ↑(Finset.image Subtype.val s) ⊆ S

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ derivative f * g

Tactic:
by

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

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
x : E
hx : x ∈ adjoin F S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
⊢ Module.rank F ↥K = 1 ↔ K = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
σ : Λ
⊢ ϕ.carrier < (L σ).carrier

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
χ : ι → R
m : M
⊢ m ∈ ⨅ i, (f i).maxGenEigenspace (χ i) ↔ ∀ (j : ι), ∃ k, ((f j - χ j • 1) ^ k) m = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
⊢ finrank F ↥K = 1 ↔ K = ⊥

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊥ = 1

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finrank F ↥⊥ = 1

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Module.rank (↥⊥) E = Module.rank F E

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
i : ι
h✝ : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo ⇑(f j) ↑p ↑p
⊢ ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
this : ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0
⊢ g (m.sum fun _μ mμ ↦ mμ) = g (m μ)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
⊢ finrank (↥K) E = 1 ↔ K = ⊤

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
⊢ IsSimpleOrder (IntermediateField F E)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ Module.rank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
x : E
⊢ finrank F ↥F⟮x⟯ = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
⊢ ⊥ = ⊤

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ (aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this✝ : Fact (Irreducible (minpoly F α))
this : F⟮α⟯.toSubfield ≤ (F⟮α⟯.toSubfield.subtype.comp f).fieldRange
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
i : ι
h : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ j, (fun j ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ j, (f j).maxGenEigenspace (μ j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ InjOn (fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}

Tactic:
by

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

Goal state before:
pp: case right.refine_1
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
x : E
hx : x ∈ Set.range ⇑(algebraMap F E)
⊢ x ∈ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

pp: case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange

Tactic:
· obtain ⟨y, hy⟩ := hx
          refine ⟨y, ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_of (aeval_gen_minpoly F α)]
          exact hy

Goal state after:
case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ {α} ⊆ ↑(F⟮α⟯.toSubfield.subtype.comp f).fieldRange
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
⊢ MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
this :
  ∀ (χ : ι → R) (s : Finset (ι → R)),
    χ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
⊢ iSupIndep fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ ?m.151

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
⊢ Function.Bijective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
h : IsIntegral F α
⊢ (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ ↑θ.carrier ∧ ∀ (i : Λ), ↑(S i) ⊆ ↑θ.carrier
⊢ restrictScalars F (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ (powerBasisAux hx) i = AdjoinSimple.gen K x ^ ↑i

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
⊢ Nonempty (E →ₐ[F] K)

Tactic:
by

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

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
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ restrictScalars F (adjoin E S) = restrictScalars F ⊤

Tactic:
by

Goal state after: