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

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
⊢ coroot ↑↑(b.baseSupportEquiv i) = b.h' i

Tactic:
let := b.isCartanSubalgebra

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ coroot ↑↑(b.baseSupportEquiv i) = b.h' i
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ ⁅b.e i, b.f i⁆ ∈ H

Tactic:
(b.sl2 i).lie_e_f,

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ b.h i ∈ H
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| X * (ascPochhammer ℕ (n + 1)).comp (X + 1)

Tactic:
ih,

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| X * (ascPochhammer ℕ n * (X + ↑n)).comp (X + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) * (X + ↑n + ↑m) = ascPochhammer S (n + (m + 1))

Tactic:
ih,

Goal state after:
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S (n + m) * (X + ↑n + ↑m) = ascPochhammer S (n + (m + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.ascFactorial b) = eval (↑a) (ascPochhammer S b)

Tactic:
← ascPochhammer_nat_eq_ascFactorial,

Goal state after:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(eval a (ascPochhammer ℕ b)) = eval (↑a) (ascPochhammer S b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| X * (descPochhammer ℤ (n + 1)).comp (X - 1)

Tactic:
ih,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| X * (descPochhammer ℤ n * (X - ↑n)).comp (X - 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ n * (X - ↑n) = (X * (ascPochhammer ℤ n).comp (X + 1)).comp (X - ↑n)

Tactic:
ih,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ (ascPochhammer ℤ n).comp (X - ↑n + 1) * (X - ↑n) = (X * (ascPochhammer ℤ n).comp (X + 1)).comp (X - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R n) * (r - ↑n) = eval (r - ↑n) (ascPochhammer R (n + 1))

Tactic:
ih,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval (r - ↑n + 1) (ascPochhammer R n) * (r - ↑n) = eval (r - ↑n) (ascPochhammer R (n + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R n * (descPochhammer R m).comp (X - ↑n) * (X - ↑n - ↑m) = descPochhammer R (n + (m + 1))

Tactic:
ih,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R (n + m) * (X - ↑n - ↑m) = descPochhammer R (n + (m + 1))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| ((interpolate s v) fun x ↦ if x ∈ s then eval (v x) f else 0) = f

Tactic:
conv =>

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| (interpolate s v) fun i ↦ eval (v i) f
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝).factorial * ↑((v x✝¹).choose ↑x✝)

Tactic:
descPochhammer_eval_eq_descFactorial ℤ _ _

Goal state after:
case e'_2
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ ↑((v x✝¹).descFactorial ↑x✝) = ↑(↑x✝).factorial * ↑((v x✝¹).choose ↑x✝)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ↑k.factorial *
      ∑ i ∈ s,
        C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j))

Tactic:
mul_sum s,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ∑ i ∈ s,
      ↑k.factorial *
        (C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j)))
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
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
i j : I
⊢ ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)

Tactic:
instLieRingModule_eq,

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
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
i j : I
⊢ ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
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
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
i j : I
⊢ ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)

Tactic:
instLieRingModule_eq,

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
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
i j : I
⊢ ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case hvs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Set.InjOn Units.val ↑(↑G).toFinset

pp: case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

pp: case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree

pp: case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

pp: case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
· exact Units.val_injective.injOn

Goal state after:
case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree

case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ 1 = (X ^ Fintype.card ↥G).leadingCoeff

Tactic:
monic_X_pow

Goal state after:
case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ 1 = 1
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
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
q : K[X]
hq : (aeval ((ad K (End K M)) (φ x))) q = (ad K (End K M)) y
⊢ ⁅y, z⁆ ∈ φ.range

Tactic:
instLieRingModule_eq,

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
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
q : K[X]
hq : (aeval ((ad K (End K M)) (φ x))) q = (ad K (End K M)) y
⊢ ⁅y, z⁆ ∈ φ.range
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝ : DecidableEq M
⊢ (weightedHomogeneousComponent w n) φ = ∑ d ∈ φ.support with (weight w) d = n, (monomial d) (coeff d φ)

Tactic:
by
  simp [weightedHomogeneousComponent, MvPolynomial, coeff, Finsupp.filter_eq_sum, support, monomial]
  congr

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : charpoly φ = X ^ finrank R M
⊢ (aeval φ) (charpoly φ) = 0

Tactic:
aeval_self_charpoly φ

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : charpoly φ = X ^ finrank R M
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (rename f) ((monomial x) (coeff x φ))).IsHomogeneous n

Tactic:
rename_monomial

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (monomial (mapDomain f x)) (coeff x φ)).IsHomogeneous n
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
x✝ : m
m✝ : n →₀ ℕ
⊢ coeff m✝ (toMvPolynomial 0 x✝) = coeff m✝ (0 x✝)

Tactic:
simp only [toMvPolynomial, zero_apply, map_zero, Finset.sum_const_zero, Pi.zero_apply]

Goal state after:
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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
h : ∀ (m : M), m ≠ 0 → φ m ≠ 0
x : M
⊢ x ∈ ker φ → x ∈ ⊥

Tactic:
simp only [mem_ker, Submodule.mem_bot]

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
h : ∀ (m : M), m ≠ 0 → φ m ≠ 0
x : M
⊢ φ x = 0 → x = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : ι → R
n : ℕ
⊢ span (Set.range x) ^ n = Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R n)

Tactic:
rw [← MvPolynomial.homogeneousSubmodule_one_pow, Submodule.map_pow,
    Ideal.span_eq_map_homogeneousSubmodule]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
hgf : IsAdjointPair B B ⇑(g * f) ⇑(f * g)
⊢ IsAdjointPair B B ⇑(f * g - g * f) ⇑(-(f * g - g * f))

Tactic:
neg_sub

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
hgf : IsAdjointPair B B ⇑(g * f) ⇑(f * g)
⊢ IsAdjointPair B B ⇑(f * g - g * f) ⇑(g * f - f * g)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
⊢ χ = X ^ r

Tactic:
suffices ∀ i < r, χ.coeff i = 0 by
    simp_rw [r, ← lieCharpoly_natDegree K E x' u] at this ⊢
    rw [(lieCharpoly_monic K E x' u).eq_X_pow_iff_natDegree_le_natTrailingDegree]
    exact le_natTrailingDegree (lieCharpoly_monic K E x' u).ne_zero this

Goal state after:
case inr.inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
⊢ ∀ i < r, χ.coeff i = 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inl.refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : α • u + x' = 0
⊢ ((toEnd K ↥U ↥E) (α • u + x')) ⟨x, ⋯⟩ = 0

Tactic:
simp only [hz₀, map_zero, LinearMap.zero_apply]

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ finrank R ↥(diagonal w).mulVecLin.range = Fintype.card { i // w i ≠ 0 }

Tactic:
← Matrix.toLin'_apply',

Goal state after:
m : Type um
R : Type uR
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ finrank R ↥(toLin' (diagonal w)).range = Fintype.card { i // w i ≠ 0 }
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
r : R
d e : Derivation R A A
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
ext a; simp only [commutator_apply, map_smul, smul_sub, smul_apply]

Goal state after: