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

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ p.degree ≠ 0

Tactic:
]

Goal state after:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ p.degree ≠ 0
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ eval (e x) p = 0

Tactic:
]

Goal state after:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ eval (e x) p = 0
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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) (C (p.coeff 0))) = (fun k ↦ eval k (C (p.coeff 0))) '' σ a

Tactic:
]

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) (C (p.coeff 0))) = (fun k ↦ eval k (C (p.coeff 0))) '' σ a
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < n

Tactic:
]

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < n
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Tactic:
]

Goal state after:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit ((aeval a) p)

Tactic:
]

Goal state after:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit ((aeval a) p)
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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ∧ ?m.44 ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ ?m.44)

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
L₁ L₂ : Lifts F E K
⊢ Prop

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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit 0

Tactic:
]

Goal state after:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit 0
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ (σ a).Nonempty

Tactic:
]

Goal state after:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ (σ a).Nonempty
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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
this : x = -(algebraMap k K) ((minpoly k x).coeff 0)
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
]

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
this : x = -(algebraMap k K) ((minpoly k x).coeff 0)
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
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
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑j).emb ((inclusion h) x)

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
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑j).emb ((inclusion h) x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ ↑s ⊆ ↑E'

Tactic:
]

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ ↑s ⊆ ↑E'
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ ↑s ⊆ ↑(restrictScalars K (adjoin L ↑s))

Tactic:
]

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ ↑s ⊆ ↑(restrictScalars K (adjoin L ↑s))
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
⊢ x ∈ adjoin F S ↔ x ∈ adjoin F S

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
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
h : FiniteDimensional K ↥(Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra)
⊢ FiniteDimensional K ↥(E1 ⊔ E2)

Tactic:
]

Goal state after:
F : Type u_1
inst✝⁷ : Field F
E : Type u_2
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
h : FiniteDimensional K ↥(Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra)
⊢ FiniteDimensional K ↥(E1 ⊔ E2)
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
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb x

Tactic:
]

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

Goal state before:
pp: case h.zero
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ m < 0,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = 0
⊢ ⊤ ≤ ⨆ μ, f.maxGenEigenspace μ

Tactic:
]

Goal state after:
case h.zero
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ m < 0,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = 0
⊢ ⊤ ≤ ⨆ μ, f.maxGenEigenspace μ
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: M : Type w
inst✝¹ : Field M
inst✝ : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
⊢ ∃ a, (fun x ↦ eval x p) a = x

Tactic:
]

Goal state after:
M : Type w
inst✝¹ : Field M
inst✝ : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
⊢ ∃ a, (fun x ↦ eval x p) a = x
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
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
⊢ E1.toSubalgebra ⊔ E2.toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
⊢ 0 < n + 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
⊢ 0 < n + 1
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
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
this : Module.rank K ↥(E1 ⊔ E2).toSubalgebra ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Tactic:
]

Goal state after:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
this : Module.rank K ↥(E1 ⊔ E2).toSubalgebra ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2
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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : adjoin F ↑S ≤ θ.carrier
⊢ False

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
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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : adjoin F ↑S ≤ θ.carrier
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
this : finrank K ↥(E1 ⊔ E2).toSubalgebra ≤ finrank K ↥E1 * finrank K ↥E2
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
]

Goal state after:
case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
this : finrank K ↥(E1 ⊔ E2).toSubalgebra ≤ finrank K ↥E1 * finrank K ↥E2
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
]

Goal state after:
case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K ↥((f.genEigenspace μ₀) ↑(n + 1))

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K ↥((f.genEigenspace μ₀) ↑(n + 1))
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case inl
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊥
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
]

Goal state after:
case inl
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊥
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case inr
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊤
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊤
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
]

Goal state after:
case inr
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h✝ : finrank F F' = 2
emb : E →ₐ[F] F'
e : E ≃ₐ[F] ↥⊤
this : IsSimpleOrder (Subalgebra F F')
h : emb.range = ⊤
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
this :
  Module.rank K ↥(Subalgebra.toSubmodule E1.toSubalgebra) ≤
    Module.rank K ↥(Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra)
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
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 = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
⊢ adjoin F (↑(↑π₁).carrier ∪ ↑S) ≤ adjoin F (↑(↑π₂).carrier ∪ ↑S)

Tactic:
]

Goal state after:
case refine_1
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 = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
⊢ adjoin F (↑(↑π₁).carrier ∪ ↑S) ≤ adjoin F (↑(↑π₂).carrier ∪ ↑S)