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

Goal state before:
pp: case refine_2
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
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ 0 = 0

pp: case refine_2.hp
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
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ minpoly F x1 ≠ 0

Tactic:
]

Goal state after:
case refine_2.hp
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
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ minpoly F x1 ≠ 0
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Tactic:
]

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g
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
⊢ K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥

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
⊢ ⊥ = ⊥

Tactic:
]

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 μ) = g (m μ)

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
⊢ Module.rank (↥⊥) E = Module.rank (↥⊥) E

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
K : IntermediateField F E
⊢ ⊤ ≤ ⊥ → ⊤ ≤ K

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ ⊤ ≤ ⊥ → ⊤ ≤ K
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 (↥⊥) E = 1 ↔ finrank (↥⊥) E = 1

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
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥

Tactic:
]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : 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
μ : ι → 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
this : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)
⊢ ⨅ i_1, Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)) =
    ⨅ i, p ⊓ (f i).maxGenEigenspace (μ i)

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
μ : ι → 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
this : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)
⊢ ⨅ i_1, Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)) =
    ⨅ i, p ⊓ (f i).maxGenEigenspace (μ i)
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
y : E
⊢ y ∈ ⊥

Tactic:
]

Goal state after:
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
y : E
⊢ y ∈ ⊥
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
y : E
⊢ y ∈ ⊥

Tactic:
]

Goal state after:
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
y : E
⊢ y ∈ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case pos
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μμ' : μ' = μ
⊢ g (m μ) = g (m μ)

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
⊢ minpoly F α = minpoly F α

Tactic:
]

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
y : F
hy : (algebraMap F E) y = x
⊢ F⟮α⟯.toSubfield.subtype (f ((AdjoinRoot.of (minpoly F α)) y)) = x

Tactic:
]

Goal state after:
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
y : F
hy : (algebraMap F E) y = x
⊢ F⟮α⟯.toSubfield.subtype (f ((AdjoinRoot.of (minpoly F α)) y)) = x
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
y : F
hy : (algebraMap F E) y = x
⊢ F⟮α⟯.toSubfield.subtype (↑(Algebra.ofId F ↥F⟮α⟯) y) = x

Tactic:
]

Goal state after:
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
y : F
hy : (algebraMap F E) y = x
⊢ F⟮α⟯.toSubfield.subtype (↑(Algebra.ofId F ↥F⟮α⟯) y) = x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
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 (f (AdjoinRoot.root (minpoly F α))) = α

Tactic:
]

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 (f (AdjoinRoot.root (minpoly F α))) = α
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
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 (AdjoinSimple.gen F α) = α

Tactic:
]

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 (AdjoinSimple.gen F α) = α
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
hχ₁₂ : ¬χ₁ = χ₂ ∧ χ₁ ∉ s
⊢ ?m.151

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 : χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : ¬χ₁ = χ₂ ∧ χ₁ ∉ s
⊢ ?m.151
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
⊢ ϕ.carrier ≤ θ.carrier ∧ α ∈ θ.carrier

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
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
⊢ ϕ.carrier ≤ θ.carrier ∧ α ∈ θ.carrier
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 α
⊢ AdjoinSimple.gen F α = AdjoinSimple.gen F α

Tactic:
]

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

Goal state before:
pp: case insert
ι : 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
⊢ ∀
    x ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        ((⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)),
    x = 0

Tactic:
]

Goal state after:
case insert
ι : 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
⊢ ∀
    x ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        ((⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)),
    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
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ AdjoinSimple.gen K x ^ ↑i = AdjoinSimple.gen K x ^ ↑i

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
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree

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
⊢ (powerBasis hx).dim = (minpoly K x).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
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 = ⊤
⊢ adjoin E S ≤ adjoin E S

Tactic:
]

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 : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
x : M
hx : x ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
hx' : x ∈ (⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
this : x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
⊢ x ∈ (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ i, (f i).maxGenEigenspace (χ₂ i)

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
x : M
hx : x ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
hx' : x ∈ (⨅ i, (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
this : x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
⊢ x ∈ (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ i, (f i).maxGenEigenspace (χ₂ 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
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (minpoly (↥x.carrier) s).degree ≠ 0

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 (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (minpoly (↥x.carrier) s).degree ≠ 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
x : E
⊢ (∃ n ∈ g.support, x = g.coeff n) → x ∈ ↑K

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
x : E
⊢ (∃ n ∈ g.support, x = g.coeff n) → x ∈ ↑K
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ m μ' ∈ (f.genEigenspace μ') ↑l₀

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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ m μ' ∈ (f.genEigenspace μ') ↑l₀
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 (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (aeval (rootOfSplits h2 ⋯)) (minpoly (↥x.carrier) s) = 0

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 (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (aeval (rootOfSplits h2 ⋯)) (minpoly (↥x.carrier) s) = 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
n : ℕ
⊢ (algebraMap (↥K) E) ((minpoly (↥K) α).coeff n) ∈ ↑K

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
n : ℕ
⊢ (algebraMap (↥K) E) ((minpoly (↥K) α).coeff n) ∈ ↑K