mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : (Polynomial.map ((↑x.emb).comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits
⊢ (Polynomial.map (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits

Tactic:
]

Goal state after:
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
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : (Polynomial.map ((↑x.emb).comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits
⊢ (Polynomial.map (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits
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
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ eval α (Polynomial.map (algebraMap (↥K') E) (g.toSubring K'.toSubring ⋯)) = 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ eval α (Polynomial.map (algebraMap (↥K') E) (g.toSubring K'.toSubring ⋯)) = 0
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
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ eval α g = 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ eval α g = 0
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
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ (aeval α) (minpoly (↥K) α) = 0

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ (aeval α) (minpoly (↥K) α) = 0
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
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K✝ : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K✝) E) (minpoly (↥K✝) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K✝
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
K : IntermediateField F E
this : finrank ↥K ↥⊤ = (minpoly (↥K) α).natDegree
⊢ finrank (↥K) E = (minpoly (↥K) α).natDegree

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K✝ : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K✝) E) (minpoly (↥K✝) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K✝
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
K : IntermediateField F E
this : finrank ↥K ↥⊤ = (minpoly (↥K) α).natDegree
⊢ finrank (↥K) E = (minpoly (↥K) α).natDegree
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
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K) α).natDegree = (minpoly (↥K) α).natDegree

Tactic:
]

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✝ : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥⊤
hn : n < finrank F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥⊤
hn : n < finrank F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E
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 : Disjoint (⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f✝ i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f✝ i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f✝ l - (algebraMap R (End R M)) (χ₂ l)
k✝ : ℕ
hk : (g ^ k✝) y = 0
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo (⇑(f - (algebraMap R (End R M)) φ))^[k] ↑p ↑p

Tactic:
]

Goal state after:
ι : 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 : Disjoint (⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f✝ i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f✝ i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f✝ l - (algebraMap R (End R M)) (χ₂ l)
k✝ : ℕ
hk : (g ^ k✝) y = 0
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo (⇑(f - (algebraMap R (End R M)) φ))^[k] ↑p ↑p
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
⊢ ∃ c, finrank K L = c * finrank K ↥K⟮x⟯

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ ∃ c, finrank K L = c * finrank K ↥K⟮x⟯
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case h
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank K L

Tactic:
]

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
f : K[X]
hi : Irreducible f
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
⊢ f.natDegree ∣ finrank K L

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hi : Irreducible f
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
⊢ f.natDegree ∣ finrank K L
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
f : K[X]
hi : Irreducible f
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
⊢ f.natDegree ∣ finrank K L

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hi : Irreducible f
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
⊢ f.natDegree ∣ finrank K L
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case neg
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ : ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0
this :
  ((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯ *
      (f - (algebraMap K (End K V)) μ') ^ l₀ =
    g
⊢ 0 = 0

Tactic:
]

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
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ (minpoly K x).natDegree ∣ finrank K L

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ (minpoly K x).natDegree ∣ finrank K L
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
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ minpoly K x ≠ 0

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ minpoly K x ≠ 0
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
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = 0
hi : minpoly K x = 0
⊢ f = 0

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = 0
hi : minpoly K x = 0
⊢ f = 0
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
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩
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
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(⨆ i, K⟮↑i⟯)

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(⨆ i, K⟮↑i⟯)
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
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
]

Goal state after:
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y
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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
x : V
hx : x ∈ ↑p
⊢ f x - μ' • x ∈ ↑p

Tactic:
]

Goal state after:
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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
x : V
hx : x ∈ ↑p
⊢ f x - μ' • x ∈ ↑p
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 α
x : K
⊢ x ∈ (minpoly F α).aroots K ↔ x ∈ (minpoly F α).aroots K

Tactic:
]

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 α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0

Tactic:
]

Goal state after:
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 α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ (aeval a) (minpoly F x) = 0

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ (aeval a) (minpoly F x) = 0
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ (adjoin.powerBasis h).dim = (minpoly F α).natDegree

pp: case h_sep
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ IsSeparable F (adjoin.powerBasis h).gen

pp: case h_splits
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ (Polynomial.map (algebraMap F K) (minpoly F (adjoin.powerBasis h).gen)).Splits

Tactic:
]

Goal state after:
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ (adjoin.powerBasis h).dim = (minpoly F α).natDegree

case h_sep
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ IsSeparable F (adjoin.powerBasis h).gen

case h_splits
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 α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits
x✝ : Fintype (↥F⟮α⟯ →ₐ[F] K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ (Polynomial.map (algebraMap F K) (minpoly F (adjoin.powerBasis h).gen)).Splits
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
x✝ : a ∈ Set.range fun ψ ↦ ψ x
ψ : K →ₐ[F] L
hψ : (fun ψ ↦ ψ x) ψ = a
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case insert.refine_2
ι : 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 : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) z ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
]

Goal state after:
case insert.refine_2
ι : 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 : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) z ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ Irreducible (Polynomial.map (algebraMap K ↥K⟮root f⟯) g - C (AdjoinSimple.gen K (root f)))

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ Irreducible (Polynomial.map (algebraMap K ↥K⟮root f⟯) g - C (AdjoinSimple.gen K (root f)))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ f = f

Tactic:
]

Goal state after: