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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval x) (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) = 0

pp: case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0

Tactic:
· exact (degree_lt_wf.min_mem _ hx).2

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r

Tactic:
have hlead := congr_arg leadingCoeff hr

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : (minpoly A x).leadingCoeff = (p * r).leadingCoeff
⊢ p = p * r
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

Tactic:
rcases le_or_gt (minpoly A x).degree 0 with h | h

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

case inr
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : 0 < (minpoly A x).degree
⊢ minpoly A x = 1
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: 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'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩
⊢ ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)

Tactic:
let fy₂ : ↥(map f I₂) := ⟨f y₂, mem_map hy₂⟩

Goal state after:
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'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩
fy₂ : ↥(map f I₂) := ⟨f y₂, ⋯⟩
⊢ ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ a ∈ I, ((Quotient.mk (map C I)).comp C) a = 0

Tactic:
by
  intro a ha
  rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
  exact mem_map_of_mem _ ha

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
this : C (i y) ∈ map (mapRingHom i) I
⊢ C y ∈ I

Tactic:
by
    obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
    refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
    rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a : R
⊢ (X + C a).Separable

Tactic:
separable_def,

Goal state after:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) (derivative (X + C a))
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.Separable

Tactic:
separable_def,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ IsCoprime X (derivative X)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
⊢ (C r).Separable ↔ IsUnit r

Tactic:
separable_def,

Goal state after:
R : Type u
inst✝ : CommSemiring R
r : R
⊢ IsCoprime (C r) (derivative (C r)) ↔ IsUnit r
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
⊢ emultiplicity q p ≤ 1

Tactic:
contrapose! hq

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ IsUnit q
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable

Tactic:
separable_def,

Goal state after:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative (f * g))
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map ((Ideal.Quotient.mk m).comp f) p).Separable
⊢ p.Separable

Tactic:
separable_def,

Goal state after:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : IsCoprime (map ((Ideal.Quotient.mk m).comp f) p) (derivative (map ((Ideal.Quotient.mk m).comp f) p))
⊢ p.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
H : derivative f = 0
HF : CharP F 0
this : CharZero F
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f

Tactic:
have := derivative_eq_zero.1 H

Goal state after:
case inl
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
H : derivative f = 0
HF : CharP F 0
this✝ : CharZero F
this : f.natDegree = 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) (b.map e)) ↑(e.symm ≪≫ₗ e) = 1

Tactic:
e.symm_trans_self,

Goal state after:
case pos.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) (b.map e)) ↑(LinearEquiv.refl A N) = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
hf : Irreducible ((expand K p) g)
⊢ False

Tactic:
revert hf

Goal state after:
case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
⊢ Irreducible ((expand K p) g) → False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f

Tactic:
separable_def,

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : IsCoprime ((expand F (p ^ n)) f) (derivative ((expand F (p ^ n)) f))
hn : n ≠ 0
hf2 : derivative ((expand F (p ^ n)) f) = 0
⊢ IsUnit f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
p n : ℕ
a : F
inst✝ : CharP F p
hn : ¬p ∣ n
ha : a ≠ 0
⊢ ↑n ≠ 0

Tactic:
rwa [← CharP.cast_eq_zero_iff F p n] at hn

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ R[root f] = ⊤

Tactic:
refine Algebra.eq_top_iff.2 fun x => ?_
  induction x using AdjoinRoot.induction_on with
    | ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
⊢ ((ad K (Module.End K V)) a).IsSemisimple

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
  have hl : Module.End.IsSemisimple (LinearMap.mulLeft K a) := by
    apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
    have : Polynomial.aeval (Algebra.lmul K (Module.End K V) a) (minpoly K a) = 0 := by
      rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
    simpa using! this
  have hr : Module.End.IsSemisimple (LinearMap.mulRight K a) := by
    apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
    have hrw : LinearMap.mulRight K a =
        (Algebra.lsmul (A := (Module.End K V)ᵐᵒᵖ) K K (Module.End K V)) (.op a) := by
      ext; simp [Algebra.lsmul]
    rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
  exact hl.sub_of_commute (LinearMap.commute_mulLeft_right a a) hr

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) ((monomial ↑i) (Pi.single i 1 i)) = root g ^ ↑i

Tactic:
rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
obtain ⟨-, hs_eq⟩ := Module.End.isNilpotent_isSemisimple_unique hn'_nil hs'_ss
    (LieAlgebra.ad_nilpotent_of_nilpotent (R := K) hn)
    (LieAlgebra.ad_isSemisimple_of_isSemisimple hs) hc'
    (LieAlgebra.commute_ad_of_commute hc) (h_jc.symm.trans (map_add (ad K _) n s))

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
hs_eq : s' = (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hJ : derivedSeriesOfIdeal R L l J = ⊥
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥

Tactic:
change D l J = ⊥ at hJ

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
D : ℕ → LieIdeal R L → LieIdeal R L := derivedSeriesOfIdeal R L
hI : D k I = ⊥
hJ : D l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_2
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ comap N.incl (lcs k N) = ⊥

Tactic:
comap_incl_eq_bot

Goal state after:
case refine_2
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ N ⊓ lcs k N = ⊥
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
⊢ ⊤ ≤ lowerCentralSeries R L L 0

Tactic:
lowerCentralSeries_zero

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ⊤ ≤ ⊤
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (m • (C r * X ^ (n + 1))) = m • eval x (C r * X ^ (n + 1))

Tactic:
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']

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

Goal state before:
pp: 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✝ : IsNilpotent L M
⊢ Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp⟩

Goal state after:
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✝ : IsNilpotent L M
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
⊢ IsTrivial L M
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:
exact N.ker_incl

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

Goal state before:
pp: 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
⊢ (∃ k, comap N.incl (ucs k ⊥) = ⊤) ↔ ∃ k, N ≤ ucs k ⊥

Tactic:
comap_incl_eq_top

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

Goal state before:
pp: 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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
⊢ IsNilpotent L ↥M₁

Tactic:
let f : L →ₗ⁅R⁆ L := LieHom.id
  let g : M₁ →ₗ[R] M₂ := Submodule.inclusion h₁
  have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
  exact (Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Singleton

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : CommSemiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra B C
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A B C
b : B
inst✝ : FaithfulSMul B C
p : A[X]
⊢ (fun a ↦ (adjoinAlgebraMap b) a = ⟨(aeval ((algebraMap B C) b)) p, ⋯⟩) ⟨(aeval b) p, ⋯⟩ ∧
    ∀ (y : ↥A[b]), (fun a ↦ (adjoinAlgebraMap b) a = ⟨(aeval ((algebraMap B C) b)) p, ⋯⟩) y → y = ⟨(aeval b) p, ⋯⟩

Tactic:
aesop (add norm [Polynomial.aeval_algebraMap_apply, Subtype.ext_iff])

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| IsIntegral F α

Tactic:
← AdjoinSimple.algebraMap_gen F α

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| IsIntegral F ((algebraMap (↥F⟮α⟯) E) (gen F α))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ x ∈ Set.range ⇑(algebraMap (↥F) L)

Tactic:
refine ⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩

Goal state after:
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ Set.range ⇑(algebraMap (↥F) L) → x ∈ F
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]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ σ ((aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
⊢ k ∈ (fun x ↦ eval x p) '' σ a

Tactic:
have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ σ ((aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
⊢ k ∈ (fun x ↦ eval x p) '' σ a
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
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
x✝¹ : Set ι
x✝ : x✝¹.Finite
⊢ FiniteDimensional K ↥(⨆ x ∈ x✝¹, t x)

Tactic:
induction Set.univ, Set.finite_univ (α := ι) using Set.Finite.induction_on with

Goal state after:
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
⊢ x1 ∈ (minpoly F x1).rootSet E

Tactic:
mem_rootSet_of_ne,

Goal state after:
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
⊢ (aeval x1) (minpoly F x1) = 0

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.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| aeval α

Tactic:
← AdjoinSimple.algebraMap_gen F α

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
| aeval ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α))
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₀ : ℕ := ⋯
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this : iSupIndep fun x ↦ (f.genEigenspace x) k
μ' : K
_hμ' : μ' ∈ m.support.erase μ
⊢ ↑l₀ ≤ k

Tactic:
obtain _ | k := k

Goal state after:
case none
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
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : 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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) none
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) none
hlk : ∀ (i : K), ↑(l i) ≤ none
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) none) ↑((f.genEigenspace μ) none)
this : iSupIndep fun x ↦ (f.genEigenspace x) none
⊢ ↑l₀ ≤ none

case some
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
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : 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 μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) (some k)
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) (some k)
hlk : ∀ (i : K), ↑(l i) ≤ some k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) (some k)) ↑((f.genEigenspace μ) (some k))
this : iSupIndep fun x ↦ (f.genEigenspace x) (some k)
⊢ ↑l₀ ≤ some k