mathlib-initiative/mathlib-tactics huggingface dataset:
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
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ f - ∑ i, (monomial ↑i) ((fun f i ↦ ((modByMonicHom hg) f).coeff ↑i) ((mk g) f) i)

Tactic:
by
        simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]
        rw [modByMonic_eq_sub_mul_div, sub_sub_cancel]
        exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
⊢ b.det (v ∘ ⇑e ∘ ⇑e.symm) = b.det v

Tactic:
e.self_comp_symm,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
⊢ b.det (v ∘ _root_.id) = b.det v
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ e.det v * ((Basis.mk hli hsp).coord k) (v k) = ↑e.det (update v k (v k))

Tactic:
mk_coord_apply_eq,

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ e.det v * 1 = ↑e.det (update v k (v k))
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hsp
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]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ y ∈ Submodule.span K (Set.range fun i ↦ root f ^ ↑i)

Tactic:
apply (isIntegral_root hf).mem_span_pow

Goal state after:
case hsp
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]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := ⋯
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ ∃ f_1, y = (aeval (root f)) f_1
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ i ∈ range (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
← sum_range_add_sum_Ico _ (Nat.le_of_succ_le h₀)

Goal state after:
case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + ∑ k ∈ Ico k (nilpotencyClass a), ((↑k !)⁻¹ • a ^ k) • m =
    ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) ((mk f) p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
quotMapOfEquivQuotMapCMapMk_symm_mk

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p) = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply,
    RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
    Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
    RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
    quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk,
    quotMapOfEquivQuotMapCMapMk_symm_mk]

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
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)

Tactic:
let lcs_eq_bot {m n} (N : LieSubmodule R L M) (le : m ≤ n) (hn : lowerCentralSeries R L N m = ⊥) :
    lowerCentralSeries R L N n = ⊥ := by
    simpa [hn] using antitone_lowerCentralSeries R L N le

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
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M),
  m ≤ n → lowerCentralSeries R L (↥N) m = ⊥ → lowerCentralSeries R L (↥N) n = ⊥ :=
  fun {m n} N le hn ↦
    Eq.mp (Eq.trans (congrArg (LE.le (lowerCentralSeries R L (↥N) n)) hn) le_bot_iff._simp_1)
      (antitone_lowerCentralSeries R L (↥N) le)
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
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⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
m : M
x : L
n✝ : x ∈ ⊤
m_n : M
h₁ : m_n ∈ lowerCentralSeries R L M k
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : ↑⁅y, n⁆ = g m
⊢ g m ∈ ⁅⊤, lowerCentralSeries R L₂ M₂ k⁆

Tactic:
← hn

Goal state after:
case succ
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⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
m : M
x : L
n✝ : x ∈ ⊤
m_n : M
h₁ : m_n ∈ lowerCentralSeries R L M k
h₂ : ⁅x, m_n⁆ = m
y : L₂
n : ↥(lowerCentralSeries R L₂ M₂ k)
hn : ↑⁅y, n⁆ = g m
⊢ ↑⁅y, n⁆ ∈ ⁅⊤, lowerCentralSeries R L₂ M₂ k⁆
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
y : L
hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L) a = y
⊢ y ∈ ↑⊥

Tactic:
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy

Goal state after:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
y : L
x : K
hxy : (algebraMap K L) x = y
⊢ y ∈ ↑⊥
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝² : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝¹ : Algebra S R := hSR.toRingHom.toAlgebra
this✝ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this : IsScalarTower R S L
⊢ { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Tactic:
haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])

Goal state after:
k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝³ : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝² : Algebra S R := hSR.toRingHom.toAlgebra
this✝¹ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this✝ : IsScalarTower R S L
this : IsScalarTower S R L
⊢ { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }
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
⊢ (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, p ⊓ (f.genEigenspace μ) k

Tactic:
suffices ∀ μ, (m μ : V) ∈ p by
    exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
⊢ ∀ (μ : K), m μ ∈ p
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
j : ι
hj : χ₁ j ≠ χ₂ j
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Tactic:
exact (End.disjoint_genEigenspace (f j) hj ⊤ ⊤).mono (iInf_le _ j) (iInf_le _ j)

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ restrictScalars F (adjoin E S) = restrictScalars F ⊤

Tactic:
restrictScalars_top,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ restrictScalars F (adjoin E S) = ⊤
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 := ⋯
this : Module.Finite K (AdjoinRoot p) := ⋯
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)
⊢ restrictScalars K (↥K⟮(aeval (root p)) g⟯)⟮root p⟯ = restrictScalars K ⊤

Tactic:
restrictScalars_top,

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)
⊢ restrictScalars K (↥K⟮(aeval (root p)) g⟯)⟮root p⟯ = ⊤
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H✝ : LieSubalgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ Nontrivial ↥H

Tactic:
by
  refine (subsingleton_or_nontrivial H).elim (fun inst ↦ False.elim ?_) id
  apply ne_bot_of_isCartanSubalgebra H
  rw [eq_bot_iff]
  exact fun x hx ↦ congr_arg Subtype.val (Subsingleton.elim (⟨x, hx⟩ : H) 0)

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
x y : L
hx : ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
hy : y ∈ H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
rw [mem_zeroRootSubalgebra] 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
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f

Tactic:
rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]

Goal state after:
case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose ⋯ ∣ f
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((↑(chainTopCoeff (-α) β) + 1) • -α + ⇑β) = ⊥

Tactic:
genWeightSpace_chainTopCoeff_add_one_zsmul_add _ _ (by simpa using hα)

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : ∀ z ∈ H, ⁅y, z⁆ = 0
⊢ y ∈ H

Tactic:
suffices y ∈ H.normalizer by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing] at this

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }
y : L
hy : (LieDerivation.ad K L) y = S'
hy' : ∀ z ∈ H, ⁅y, z⁆ = 0
⊢ y ∈ H.normalizer
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
this : K ∙ coroot α = K ∙ α'
⊢ ↑(corootSpace ⇑α) = K ∙ coroot α

Tactic:
coe_corootSpace_eq_span_singleton'

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
this : K ∙ coroot α = K ∙ α'
⊢ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) = K ∙ coroot α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (T R (↑n + 1))
ih2 : eval (-x) (T R ↑n) = ↑↑(↑n).negOnePow * eval x (T R ↑n)
⊢ eval (-x) (T R (↑n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n))

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (T R (↑n + 1))
ih2 : eval (-x) (T R ↑n) = ↑↑(↑n).negOnePow * eval x (T R ↑n)
⊢ -(2 * x) * (-↑↑((↑n).negOnePow * 1) * eval x (T R (↑n + 1))) - ↑↑(↑n).negOnePow * eval x (T R ↑n) =
    ↑↑((↑n).negOnePow * 1) * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
this : U R (0 + 2) = 2 * X * U R (0 + 1) - U R 0
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
simp only [zero_add, U_one, U_zero] at this

Goal state after:
R : Type u_1
inst✝ : CommRing R
this : U R 2 = 2 * X * (2 * X) - 1
⊢ U R 2 = 4 * X ^ 2 - 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : ↑m ≠ -1
⊢ (U R ↑m).degree = ↑((↑m + 1).natAbs - 1)

pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑m ≠ -1
⊢ (U R (-↑m)).degree = ↑((-↑m + 1).natAbs - 1)

Tactic:
case inl => rw [degree_U_natCast R m]; norm_cast

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑m ≠ -1
⊢ (U R (-↑m)).degree = ↑((-↑m + 1).natAbs - 1)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
⊢ (killingForm K L).restrict H.toSubmodule =
    ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)

Tactic:
restrict_killingForm,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
⊢ traceForm K (↥H) L = ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : M
⊢ -x ∈ range ⇑P.root ↔ x ∈ range ⇑P.root

Tactic:
suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root by
    refine ⟨this x, fun h ↦ ?_⟩
    rw [← neg_neg x] at h
    exact this (-x) h
  intro y ⟨i, hi⟩
  exact ⟨P.reflectionPerm i i, by simp [neg_eq_iff_eq_neg.mpr hi]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
⊢ ∀ {F : Dual R M},
    MapsTo (⇑(preReflection x F)) Φ Φ → MapsTo (⇑(preReflection x' ((span R Φ).subtype.dualMap F))) Φ' Φ'

Tactic:
intro F hF ⟨y, hy⟩ hy'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Finite ↑Φ
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : span R Φ' = ⊤
x' : ↥(span R Φ) := ⟨x, hx⟩
F : Dual R M
hF : MapsTo (⇑(preReflection x F)) Φ Φ
y : M
hy : y ∈ span R Φ
hy' : ⟨y, hy⟩ ∈ Φ'
⊢ (preReflection x' ((span R Φ).subtype.dualMap F)) ⟨y, hy⟩ ∈ Φ'