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

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
b : P.Base
inst✝ : P.IsRootSystem
⊢ ⊤ ≤ span R (range (⇑P.root ∘ Subtype.val))

Tactic:
simp [range_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inl
ι : 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
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
pos : 0 < f
⊢ ∑ j ∈ b.support, f j ≠ 0

Tactic:
refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'
    by_contra! contra
    replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (contra j (hf₀ hj)) (pos.le j)
      · simpa using hj
    exact P.ne_zero i <| by simp [hf₂, contra]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case pos
ι : 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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j * (B.form (P.root j)) (P.root j) = P.pairing j i * (B.form (P.root i)) (P.root i)
⊢ P.pairing i j = P.pairing j i

Tactic:
h i j,

Goal state after:
case pos
ι : 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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j * (B.form (P.root j)) (P.root j) = P.pairing j i * (B.form (P.root j)) (P.root j)
⊢ P.pairing i j = P.pairing j i
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : Cauchy abs
⊢ { cauchy := f⁻¹ } = { cauchy := f }.inv'

Tactic:
rw [inv']

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : Cauchy abs
⊢ { cauchy := f }.inv'.cauchy = { cauchy := f }.cauchy⁻¹

Tactic:
rw [inv']

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (f.inv ⋯) = mk (g.inv ⋯)

Tactic:
← mul_one (mk (inv f hf)),

Goal state after:
case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (f.inv hf) * 1 = mk (g.inv ⋯)
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < star v ⬝ᵥ v ↔ v ≠ 0

Tactic:
nontriviality R
  refine (Fintype.sum_pos_iff_of_nonneg fun i => star_mul_self_nonneg _).trans ?_
  simp_rw [Pi.lt_def, Function.ne_iff, Pi.zero_apply]
  refine (and_iff_right fun i => star_mul_self_nonneg (v i)).trans <| exists_congr fun i => ?_
  constructor
  · rintro h hv
    simp [hv] at h
  · exact (star_mul_self_pos <| .of_ne_zero ·)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k

Tactic:
mulVec,

Goal state after:
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ (fun j ↦ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M.PosSemidef ↔ M.IsHermitian ∧ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
by
  simp [PosSemidef, ← Finsupp.equivFunOnFinite.forall_congr_right, dotProduct, mulVec,
    Finsupp.sum_fintype, Finset.mul_sum, mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : Fintype n
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M ^ (k + 2)).PosSemidef

Tactic:
by
    rw [pow_succ, pow_succ']
    simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mpr.ha
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr) ᵥ* A ⬝ᵥ (x ∘ Sum.inl + (A⁻¹ * B) *ᵥ x ∘ Sum.inr)

pp: case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
· rw [← dotProduct_mulVec]
      apply (posSemidef_iff_dotProduct_mulVec.mp hA.posSemidef).2

Goal state after:
case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬(4 - b.cartanMatrix).det = 0

Tactic:
← det_toLin',

Goal state after:
ι : 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
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬LinearMap.det (toLin' (4 - b.cartanMatrix)) = 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
⊢ (4 - b.cartanMatrix).det ≠ 0

Tactic:
by
  suffices ¬ HasEigenvalue b.cartanMatrix.toLin' 4 by
    have aux : (4 - b.cartanMatrix).toLin' = - (b.cartanMatrix.toLin' - (4 : ℤ) • 1) := by ext; simp
    rwa [ne_eq, ← det_toLin', det_eq_zero_iff_ker_ne_bot, aux, ker_neg, ← eigenspace_def,
      ← hasEigenvalue_iff]
  obtain ⟨d, hd, hdS⟩ := b.exists_cartanMatrix_diagaonal_mul_posDef
  have aux (i j : b.support) : b.cartanMatrix i j ≤ if i = j then 2 else 0 := by
    rcases eq_or_ne i j with rfl | hij
    · simp
    · simpa [hij] using cartanMatrix_le_zero_of_ne b i j hij
  have := b.cartanMatrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen d hdS hd 2 4 aux
  aesop

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

Goal state before:
pp: case refine_1
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
a : R
⊢ ((aeval f) (C a)) x = eval μ (C a) • x

Tactic:
simp [Module.algebraMap_end_apply]

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
⊢ (minpoly R f).IsRoot μ

Tactic:
rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩
  refine Or.resolve_right (smul_eq_zero.1 ?_) ne0
  rw [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩]
  simp

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
hq : minpoly R f = (X - C μ) * 0
h_contra : ∀ (v : M), ((aeval f) 0) v = 0
this : 1 + degree 0 ≤ degree 0
⊢ False

Tactic:
exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
v : M
hv : ((aeval f) q) v ≠ 0
⊢ ((aeval f) q) v ∈ f.eigenspace μ

Tactic:
simpa [sub_eq_zero, hq] using congr($(minpoly.aeval R f) v)

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ ↑(#s - 1) < ↑(#s)

Tactic:
WithBot.coe_lt_coe

Goal state after:
case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ #s - 1 < #s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ↑0 < ↑(#s)

Tactic:
WithBot.coe_lt_coe

Goal state after:
case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ 0 < #s
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
h₁ : range b₁.e = range (⇑p₁ ∘ prodE eι b₁ b₂)
h₂ : range b₁.f = range (⇑p₁ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₁ (range (⇑p₁ ∘ prodE eι b₁ b₂) ∪ range (⇑p₁ ∘ prodF eι b₁ b₂)) ≤
    lieSpan R L₁ (⇑p₁ '' range (prodE eι b₁ b₂) ∪ ⇑p₁ '' range (prodF eι b₁ b₂))

Tactic:
simp [range_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ↑(#s - 1) < ↑(#s)

Tactic:
WithBot.coe_lt_coe

Goal state after:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ #s - 1 < #s
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
h₂ : range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)
⊢ lieSpan R L₂ (range (⇑p₂ ∘ prodE eι b₁ b₂) ∪ range (⇑p₂ ∘ prodF eι b₁ b₂)) ≤
    lieSpan R L₂ (⇑p₂ '' range (prodE eι b₁ b₂) ∪ ⇑p₂ '' range (prodF eι b₁ b₂))

Tactic:
simp [range_comp]

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

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hns : s ∈ K[φ x]
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
⊢ _root_.IsNilpotent (φ x)

Tactic:
replace hns : Commute n s :=
    commute_of_mem_adjoin_singleton_of_commute hns (commute_of_mem_adjoin_self hn_adj).symm

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
⊢ _root_.IsNilpotent (φ x)
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)

Tactic:
rw [← Submodule.map_le_iff_le_comap]
    apply le_sup_of_le_left
    rw [Submodule.map_le_iff_le_comap]
    intro y hy
    simp only [Submodule.mem_comap, mem_engel_iff, mem_toSubmodule]
    use k + 1
    clear hk; revert hy
    generalize k + 1 = k
    induction k generalizing y with
    | zero =>
      cases y; intro hy; simp only [pow_zero, Module.End.one_apply]
      exact (AddSubmonoid.mk_eq_zero N.toAddSubmonoid).mp hy
    | succ k ih => solve_by_elim

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal

Tactic:
iSup,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (sSup (range fun i ↦ s i)).toIdeal = ⨆ i, (s i).toIdeal
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ (⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal

Tactic:
toIdeal_iSup

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2.add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x p q : MvPolynomial σ R
hp✝ : IsWeightedHomogeneous 1 p n
hq✝ : IsWeightedHomogeneous 1 q n
hp : p ∈ homogeneousSubmodule σ R 1 ^ n
hq : q ∈ homogeneousSubmodule σ R 1 ^ n
⊢ p + q ∈ homogeneousSubmodule σ R 1 ^ n

Tactic:
| add p q _ _ hp hq =>

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I) =
    (⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }).toIdeal

Tactic:
toIdeal_iSup

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I) =
    ⨆ i, toIdeal { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
⊢ [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥,
      ∀ (m : M), φ m = 0 → m = 0].TFAE

Tactic:
have := (hasEigenvalue_zero_tfae φ).not

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
this :
  (List.map Not
      [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < ker φ,
        ∃ m, m ≠ 0 ∧ φ m = 0]).TFAE
⊢ [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥,
      ∀ (m : M), φ m = 0 → m = 0].TFAE
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ ∑ x ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff x) +
      constantCoeff (((finSuccEquiv R N) F).coeff n) ≠
    0

Tactic:
Finset.sum_eq_zero aux,

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ 0 + constantCoeff (((finSuccEquiv R N) F).coeff n) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
x : DirectSum M fun i ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (decompose' R w ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) x)) m = x m

Tactic:
← Subtype.coe_inj,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
x : DirectSum M fun i ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ ↑((decompose' R w ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) x)) m) = ↑(x m)
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: case mem
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
h : ∃ a a_1, ⁅a, a_1⁆ = y
⊢ χ y = 0

Tactic:
obtain ⟨z, w, rfl⟩ := h

Goal state after:
case mem
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x z w : L
⊢ χ ⁅z, w⁆ = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ φ.IsNilRegular x ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
rw [isNilRegular_def]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
⊢ ∃ x, φ.IsNilRegular x

Tactic:
by
  let b := chooseBasis R L
  let bₘ := chooseBasis R M
  let n := Fintype.card (ChooseBasisIndex R M)
  have aux :
    ((polyCharpoly φ b).coeff (nilRank φ)).IsHomogeneous (n - nilRank φ) :=
    polyCharpoly_coeff_isHomogeneous _ b (nilRank φ) (n - nilRank φ)
      (by simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex])
  obtain ⟨x, hx⟩ : ∃ r, eval r ((polyCharpoly _ b).coeff (nilRank φ)) ≠ 0 := by
    by_contra! h₀
    apply polyCharpoly_coeff_nilRank_ne_zero φ b
    apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
    simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]
  let c := Finsupp.equivFunOnFinite.symm x
  use b.repr.symm c
  rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]

Goal state after: