mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (aeval ((aeval f) p)) (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) = 0

Tactic:
← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
        fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h,

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (aeval
        (((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯).comp
            (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})))
          p))
      (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) =
    0
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: 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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
⊢ Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)

Tactic:
by
  intro _ hx
  induction hx using LieSubalgebra.lieSpan_induction with
  | mem x hx => exact h hx
  | zero => simp
  | add x y _ _ hx hy => simp [hx, hy]
  | smul t x _ hx => simp [hx]
  | lie x y _ _ hx hy => simp [hx, hy]

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣ (aeval (P.newtonMap^[n + 1] x)) P

Tactic:
rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (x - y) ^ p

Tactic:
← neg_sub y x,

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (-(y - x)) ^ p
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤
⊢ derivedSeriesOfIdeal R L 1 ⊤ = ⊤

Tactic:
rw [← ih, eq_top_iff]

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤
⊢ ⊤ ≤ derivedSeriesOfIdeal R L (n + 1) ⊤
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
⊢ let S := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)

Tactic:
S

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
⊢ ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩

Goal state after:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, (LieSubmodule.Quotient.mk' H.toLieSubmodule) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
⊢ let S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)

Tactic:
S

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
⊢ ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L
⊢ ⁅Quotient.mk'' x, Quotient.mk'' x⁆ = 0

Tactic:
rw [is_quotient_mk, ← mk_bracket]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L
⊢ mk ⁅x, x⁆ = 0
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: 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
g : M
x : F
hx : x ∈ subfield M F
g' : M
⊢ g' • g • x = g • x

Tactic:
by rw [hx, hx]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ i ∈ s, l i ∈ subfield G F
hla : ∑ x ∈ s, l x • (toFun G F) x 1 = (toFun G F) a 1
⊢ False

Tactic:
toFun_apply,

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ i ∈ s, l i ∈ subfield G F
hla : ∑ x ∈ s, l x • 1 • x = 1 • a
⊢ False
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x✝ : ↥(toAlgHom F E K₁).range
x : K₂
y : K₁
hx : ↑ϕ y = x
z : E
hy : (toAlgHom F E K₁).toRingHom z = y
⊢ ↑ϕ ((toAlgHom F E K₁).toRingHom z) ∈ (toAlgHom F E K₂).range

Tactic:
apply minpoly.mem_range_of_degree_eq_one E

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x✝ : ↥(toAlgHom F E K₁).range
x : K₂
y : K₁
hx : ↑ϕ y = x
z : E
hy : (toAlgHom F E K₁).toRingHom z = y
⊢ (minpoly E (↑ϕ ((toAlgHom F E K₁).toRingHom z))).degree = 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case f
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
x : F
| g • l x * (toFun G F) x g'

Tactic:
toFun_apply,

Goal state after:
case f
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
x : F
| g • l x * g' • x
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • (toFun G F) a (g⁻¹ * g') = (toFun G F) a g'

Tactic:
toFun_apply,

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • (g⁻¹ * g') • a = (toFun G F) a g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • (g⁻¹ * g') • a = (toFun G F) a g'

Tactic:
toFun_apply,

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • (g⁻¹ * g') • a = g' • a
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ (Polynomial.map (algebraMap K L) p).Splits

Tactic:
rw [← f.toAlgHom.comp_algebraMap, ← map_map]
    exact (splits F p).map _

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = (↑f).range

Tactic:
(splits F p).adjoin_rootSet_eq_range,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet F) = ⊤
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
K : IntermediateField F E
α : ↥K
⊢ lift (adjoin F {α}) = adjoin F {↑α}

Tactic:
simp only [lift_adjoin, Set.image_singleton]

Goal state after:
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:
apply e.symm.injective

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) = e.symm 0
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
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x

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 : (aeval x) (minpoly k x) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
a✝ : Nontrivial A
a : 𝕜
ha : a ∈ (fun x ↦ eval x (X ^ 2 - X)) ⁻¹' spectrum 𝕜 ((aeval p) (X ^ 2 - X))
⊢ a ^ 2 = a

Tactic:
simpa [pow_two p, hp.eq, sub_eq_zero] using ha

Goal state after:
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 → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
this : IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)
⊢ ↑S ⊆ ↑(union (Set.range θ) this).carrier

Tactic:
carrier_union,

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 → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
this : IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)
⊢ ↑S ⊆ ↑(⨆ i, (↑i).carrier)
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
rw [map_add, hk, zero_add]

Goal state after:
case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) z ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯

Tactic:
exact (adjoinRootEquivAdjoin K hx.isIntegral).symm.trans <|
    (AdjoinRoot.algEquivOfEq _ _ _ h_mp).trans (adjoinRootEquivAdjoin K hy.isIntegral)

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
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
y : ↥H
⊢ x ∈ genWeightSpaceOf L (χ₁ y) y

Tactic:
rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx

Goal state after:
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 : ∀ (i : ↥H), x ∈ genWeightSpaceOf L (χ₁ i) i
hm : m ∈ genWeightSpace M χ₂
y : ↥H
⊢ x ∈ genWeightSpaceOf L (χ₁ y) y
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
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Tactic:
refine le_antisymm ?_ (LieSubalgebra.le_normalizer _)
  intro x hx
  rw [LieSubalgebra.mem_normalizer_iff] at hx
  rw [mem_zeroRootSubalgebra]
  rintro ⟨y, hy⟩
  specialize hx y (le_zeroRootSubalgebra R L H hy)
  rw [mem_zeroRootSubalgebra] at hx
  obtain ⟨k, hk⟩ := hx ⟨y, hy⟩
  rw [← lie_skew, map_neg, neg_eq_zero] at hk
  use k + 1
  rw [Module.End.iterate_succ, LinearMap.coe_comp, Function.comp_apply, toEnd_apply_apply,
    LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, hk]

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

Goal state before:
pp: case pos
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α

pp: case neg
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α

Tactic:
· rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule by ext; simp [hα.eq]]
      exact le_sup_left

Goal state after:
case neg
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ LieSubmodule.restr I H ⊓ genWeightSpace L ⇑α ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α