mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0

Tactic:
weightedTotalDegree,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ (p.support.sup fun s ↦ (weight w) s) = 0
Module: Mathlib.Algebra.Lie.Matrix

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type w₁
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
x✝¹ x✝ : Matrix n n R
⊢ (reindex e e) ⁅x✝¹, x✝⁆ = ⁅(reindex e e) x✝¹, (reindex e e) x✝⁆

Tactic:
simp only [LieRing.of_associative_ring_bracket, Matrix.reindex_apply,
        Matrix.submatrix_mul_equiv, Matrix.submatrix_sub, Pi.sub_apply]

Goal state after:
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
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
⊢ ∃ x, φ.IsNilRegular x

Tactic:
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]

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
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
⊢ ∃ x, φ.IsNilRegular x
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: case mp
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) →
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x

pp: case mpr
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s

Tactic:
· rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
    exact ⟨t, rfl, si⟩

Goal state after:
case mpr
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval fun i ↦ (b.repr y) i * r + (b.repr x) i)) ((↑φ).polyCharpoly b) =
    charpoly (φ (r • y) + φ x)

Tactic:
aux,

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval ⇑(b.repr (r • y + x)))) ((↑φ).polyCharpoly b) = charpoly (φ (r • y) + φ x)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: 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
this : LinearMap.charpoly ((toEnd K ↥U ↥E) y') = X ^ finrank K ↥E
⊢ Ex ≤ Ey

Tactic:
LinearMap.charpoly_eq_X_pow_iff,

Goal state after:
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
this : ∀ (m : ↥E), ∃ n, ((toEnd K ↥U ↥E) y' ^ n) m = 0
⊢ Ex ≤ Ey
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R

Tactic:
by
  rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R),
    fromBlocks_smul, Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
  simp [fromBlocks]

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

Goal state before:
pp: 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} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
hi : 0 < r
⊢ ∀ (r : K), eval r (χ.coeff 0) = 0

pp: case deg
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
⊢ ↑(χ.coeff 0).natDegree < #K

Tactic:
case deg =>
      -- We need to show `(natDegree (coeff χ 0)) < #K` and know that `finrank K L ≤ #K`
      apply lt_of_lt_of_le _ hLK
      rw [Nat.cast_lt]
      -- So we are left with showing `natDegree (coeff χ 0) < finrank K L`
      apply lt_of_le_of_lt _ hr
      apply lieCharpoly_coeff_natDegree _ _ _ _ 0 r (zero_add r)

Goal state after:
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} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
hi : 0 < r
⊢ ∀ (r : K), eval r (χ.coeff 0) = 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
Matrix.det_transpose

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit A.det
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * M *
      (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod =
    diagonal fun i ↦ if i ∈ s then 1 else 0

Tactic:
hM0,

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod *
        ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod) *
      (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod =
    diagonal fun i ↦ if i ∈ s then 1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod *
      ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod *
        (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod) =
    diagonal fun i ↦ if i ∈ s then 1 else 0

Tactic:
mul_assoc _ (L'.map _).prod,

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod *
      ((List.map toMatrix L).prod * diagonal D *
        ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)) =
    diagonal fun i ↦ if i ∈ s then 1 else 0
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.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
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
α : K
hα : α ∈ s ∧ (constantCoeff ψ ≠ 0 → ¬eval α (constantCoeff ψ) = 0)
⊢ eval α (constantCoeff ψ) ≠ 0

Tactic:
exact hα.2 hψ

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝ : A
l : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝ ⊗ₜ[R] l, y⁆ =
    ⁅x✝ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l)⁆

Tactic:
refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
          · simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]
          · simp [h1, h2, sub_add_sub_comm]

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

Goal state before:
pp: case neg
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : ¬j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) i = ⁅x, (lof R ι M j).toFun m⁆ i

Tactic:
simp only [lof, lsingle, AddHom.toFun_eq_coe, lie_module_bracket_apply]
        -- The coercion in the goal is `DFunLike.coe (β := fun x ↦ Π₀ (i : ι), M i)`
        -- but the lemma is expecting `DFunLike.coe (β := fun x ↦ ⨁ (i : ι), M i)`
        erw [AddHom.coe_mk]
        simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det

Tactic:
have hF' : IsUnit F' := by
    refine F'.isUnit_iff_isUnit_det.2 ?_
    convert (symplectic_det hA).map f
    rw [RingHom.map_det, RingHom.mapMatrix_apply, Matrix.fromBlocks_map]; rfl

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h.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
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) (α • u + x')) (((toEnd K (↥U) Q) v ^ k) z') = 0

Tactic:
rw [← hn, hk, pow_succ', Module.End.mul_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (decompose ℒ).symm ⁅x, y⁆ = ⁅(decompose ℒ).symm x, (decompose ℒ).symm y⁆

Tactic:
simp only [← decomposeLinearEquiv_symm_apply]

Goal state after:
ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ).symm ⁅x, y⁆ = ⁅(decomposeLinearEquiv ℒ).symm x, (decomposeLinearEquiv ℒ).symm y⁆
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ b ∈ (lof R ι (fun x ↦ ↥(ℒ x)) k).range

Tactic:
use ⟨(decompose ℒ).symm b, hb⟩

Goal state after:
case h
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ (lof R ι (fun x ↦ ↥(ℒ x)) k) ⟨(decompose ℒ).symm b, hb⟩ = b
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: case hadd
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f i = 0
a✝ : a ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) ⁅f, y⁆) j) =
    ↑(⁅f, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) y⁆ j) -
      ↑(⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆ j)
⊢ ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, y⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) y⁆
          j) -
      ↑(⁅y, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)

Tactic:
clear ih

Goal state after:
case hadd
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f i = 0
a✝ : a ≠ 0
⊢ ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, y⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) y⁆
          j) -
      ↑(⁅y, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
hχ : Nontrivial ↥(weightSpace M ⇑χ)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
replace hχ : Nontrivial N := hχ

Goal state after:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : Nontrivial ↥N
⊢ HasCentralRadical k L ∧ ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id