mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
h : Subsingleton M
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥

Tactic:
← not_nontrivial_iff_subsingleton

Goal state after:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
h : ¬Nontrivial M
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≠
    ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
hI₂ : R ∙ ⟨x, hxK'⟩ ⊔ ↑I = ⊤
e : ↥K ≃ₗ⁅R⁆ ↥I
hI₃ : IsEngelian R ↥I
⊢ LieModule.IsNilpotent (↥K') M

Tactic:
exact LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ ↑(lowerCentralSeries R (↥(toEnd R L M).range) M 0) = ↑(lowerCentralSeries R L M 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
⊢ ucs 0 N₁ ≤ ucs 0 N₂

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
⊢ ucs 0 N₁ = N₁

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
l : ℕ
⊢ lcs (l + 0) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs 0 N₂

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ comap N.incl (ucs 0 ⊥) = ucs 0 ⊥

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
⊢ Submodule.map g ↑(lowerCentralSeries R L M 0) ≤ ↑(lowerCentralSeries R L₂ M₂ 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝ : LieModule R L₂ M₂
hf_surj : Surjective ⇑f
hg_surj : Surjective ⇑g
⊢ ↑(lowerCentralSeries R L₂ M₂ 0) ≤ Submodule.map g ↑(lowerCentralSeries R L M 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R L (L ⧸ I) 0) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R (↥I) (↥I) 0) ≤ ↑(lowerCentralSeries R L (↥I) 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L 0) = lowerCentralSeries R L' L' 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
inst✝ : LieModule R L M
⊢ ↑(I.lcs M 0) = ↑(lowerCentralSeries R (↥I) M 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0 = baseChange A (lowerCentralSeries R L M 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (Polynomial.map (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x)).Splits

Tactic:
← minpoly_eq_minpoly,

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (Polynomial.map (algebraMap (↥(subfield G F)) F) (minpoly G F x)).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (_root_.minpoly (↥(subfield G F)) x).Separable

Tactic:
← minpoly_eq_minpoly,

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (minpoly G F x).Separable
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
by_cases h : Module.Finite R A ∧ Module.Finite R B
  · obtain ⟨_, _⟩ := h
    simpa only [map_mul] using! Cardinal.toNat_le_toNat (A.rank_sup_le_of_free B)
      (Cardinal.mul_lt_aleph0 (rank_lt_aleph0 R A) (rank_lt_aleph0 R B))
  wlog hA : ¬ Module.Finite R A generalizing A B
  · have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA))
    rwa [sup_comm, mul_comm] at this
  rw [← rank_lt_aleph0_iff, not_lt] at hA
  have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp
  rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,
    show finrank R ↥(A ⊔ B) = 0 from Cardinal.toNat_apply_of_aleph0_le (hA.trans this), zero_mul]

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (⨆ i, S i).FG

Tactic:
← hs,

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (⨆ i, adjoin F ↑(s i)).FG
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₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

Tactic:
by
  rw [lt_iff_le_and_ne, and_congr_right]; intro h; simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]

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'
⊢ restrictScalars K E' ≤ restrictScalars K (adjoin L ↑s)

Tactic:
← hs,

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'
⊢ adjoin K ↑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
α x : E
⊢ x ∈ F⟮α⟯ ↔ ∃ r s, x = (aeval α) r / (aeval α) s

Tactic:
by
  simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

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
      rw [minpoly.algHom_eq f f.injective]; exact hL x

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
⊢ (adjoinRootEquivAdjoin K hx) (AdjoinRoot.powerBasis ⋯).gen ^ ↑i = AdjoinSimple.gen K x ^ ↑i

Tactic:
AdjoinRoot.powerBasis_gen,

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
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ (adjoinRootEquivAdjoin K hx) (AdjoinRoot.root (minpoly K x)) ^ ↑i = AdjoinSimple.gen K x ^ ↑i
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case zero
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
⊢ ∃ L, FiniteDimensional F ↥L ∧ 0 < finrank F ↥L

Tactic:
| zero =>

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
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 : ι
⊢ ∃ k,
    ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)

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
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,
    ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ 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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
⊢ IsIntegral K ((aeval (root p)) g)

Tactic:
exact IsIntegral.of_finite _ _

Goal state after:
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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝¹ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this✝ : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
this : (↥K⟮(aeval (root p)) g⟯)⟮root p⟯ = ⊤
⊢ IsIntegral (↥K⟮(aeval (root p)) g⟯) (root p)

Tactic:
exact IsIntegral.of_finite _ _

Goal state after:
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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
⊢ p.natDegree = f.natDegree * g.natDegree

Tactic:
have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g := by
    trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
    · have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
      rw [← finrank_top', ← this, adjoin.finrank]
      exact IsIntegral.of_finite _ _
    · simp [← key₂]

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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
key₂' : finrank (↥K⟮(aeval (root p)) g⟯) Kx = g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ LieSubmodule.ucs 0 H.toLieSubmodule = H.toLieSubmodule

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hy : y ∈ span R {e, f, h}
⊢ ⁅0, y⁆ ∈ span R {e, f, h}

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u : L
hu : u ∈ {e, f, h}
⊢ ⁅u, 0⁆ ∈ span R {e, f, h}

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : ∀ (i : ↥H), m ∈ genWeightSpaceOf M (χ₂ i) i
y : ↥H
hx : x ∈ genWeightSpaceOf L (χ₁ y) y
⊢ m ∈ genWeightSpaceOf M (χ₂ y) y

Tactic:
exact hm y

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ((toEnd R L M) x ^ 0) m ∈ genWeightSpace M (0 • χ₁ + χ₂)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅0, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
⊢ ⁅h, ((toEnd R L M) f ^ 0) m⁆ = (μ - 2 * ↑0) • ((toEnd R L M) f ^ 0) m

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case pos.zero
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
⊢ ⁅u, 0⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
⊢ ⁅e, ((toEnd R L M) f ^ (0 + 1)) m⁆ = ((↑0 + 1) * (μ - ↑0)) • ((toEnd R L M) f ^ 0) m

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
⊢ ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
change (g ^ k).comp (H : Submodule R L).subtype ⟨x, hx⟩ = 0

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
⊢ ((g ^ k) ∘ₗ H.subtype) ⟨x, hx⟩ = 0