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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅⁅e, f⁆, ((toEnd R L M) f ^ (n + 1)) m⁆ + ⁅f, ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆⁆ =
    ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m

Tactic:
t.lie_e_f,

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ((toEnd R L M) f ^ (n + 1)) m⁆ + ⁅f, ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆⁆ =
    ((↑(n + 1) + 1) * (μ - ↑(n + 1))) • ((toEnd R L M) f ^ (n + 1)) m
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
⊢ (rootSpaceWeightSpaceProductAux R L H M hχ).toFun ⁅x, y⁆ = ⁅x, (rootSpaceWeightSpaceProductAux R L H M hχ).toFun y⁆

Tactic:
by
        ext m
        simp only [rootSpaceWeightSpaceProductAux]
        dsimp
        simp only [lie_lie]

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

Goal state before:
pp: case h
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 : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ = 0
⊢ (H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0

Tactic:
simp only [Submodule.subtype_apply, Function.comp_apply, Module.End.pow_apply, LinearMap.coe_comp,
    Submodule.coe_eq_zero]

Goal state after:
case h
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 : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ = 0
⊢ (⇑f)^[k] ⟨x, hx⟩ = 0
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 : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
rintro ⟨y, hy⟩

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : IsNoetherian R M
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
⊢ ((toEnd R L M) f ^ (n + 1)) m = 0

Tactic:
by
  by_contra h
  have : t.HasPrimitiveVectorWith (ψ (n + 1)) (n - 2 * (n + 1) : R) :=
    { ne_zero := h
      lie_h := (P.lie_h_pow_toEnd_f _).trans (by simp [hn])
      lie_e := (P.lie_e_pow_succ_toEnd_f _).trans (by simp [hn]) }
  obtain ⟨m, hm⟩ := this.exists_nat
  have : (n : ℤ) < m + 2 * (n + 1) := by lia
  exact this.ne (Int.cast_injective (α := R) <| by simpa [sub_eq_iff_eq_add] using hm)

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      LieSubmodule.map H.toLieSubmodule.incl
        (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
            ⋯).range ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}

Tactic:
← LieModuleHom.map_top,

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      LieSubmodule.map H.toLieSubmodule.incl
        (LieSubmodule.map
          (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯)
          ⊤) ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
⊢ H = lieSpan R L (range (-b.h))

Tactic:
by
    rw [← neg_range', lieSpan_neg]
    exact b.cartan_eq_lieSpan

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
hx : x ∈ H
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅x, t • u⁆ ∈ lieSpan R L (range b.e)

Tactic:
| smul t u _ hu =>

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (Finsupp.single j 1) i = if j = i then 1 else 0

Tactic:
Finsupp.single_apply

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (if j = i then 1 else 0) = if j = i then 1 else 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, t • u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
| smul t u _ hu =>

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

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
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)

Tactic:
simp only [LieIdeal.toLieSubalgebra_toSubmodule, orthogonal_toSubmodule,
    LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]

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
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (Φ.orthogonal ↑I) ↑I
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S

Tactic:
apply _root_.sSup_le
    rintro _ ⟨c, -, h₁, h₂, rfl⟩
    apply hT₁

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ⊥ ≠ ⊤
⊢ ∃ x y, x ≠ y

Tactic:
contrapose! aux

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
⊢ ⊥ = ⊤
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅t • u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| smul t u _ hu =>

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h✝ : x = v ∧ ↑hx = count v m
⊢ (none.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) = ⟨x, hx⟩

Tactic:
rename_i h

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h : x = v ∧ ↑hx = count v m
⊢ (none.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) = ⟨x, hx⟩
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (toSplittingField s) ((subProdXSubC f).coeff n) = 0

Tactic:
simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub,
    Polynomial.map_prod, Polynomial.map_sub, map_X, map_C, toSplittingField,
    AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h,
    ← (finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]
  rw [Finset.prod_coe_sort (f := fun x : _ × ℕ ↦ X - C x.1), (Multiset.toEnumFinset _)
    |>.prod_eq_multiset_prod, ← Function.comp_def (X - C ·) Prod.fst, ← Multiset.map_map,
    Multiset.map_toEnumFinset_fst, map_map, AlgHom.comp_algebraMap]
  conv in map _ _ => rw [Splits.eq_prod_roots (Monics.splits_finsetProd h)]
  rw [leadingCoeff_map, f.2, map_one, C_1, one_mul, sub_self, coeff_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
⊢ ↑(tensorDistribEquiv R) = tensorDistrib R R

Tactic:
ext B₁ B₂ : 3
  ext
  exact mul_comm _ _

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I = ⊥

Tactic:
by
  rw [eq_bot_iff, ← killingCompl_top_eq_bot]
  exact I.le_killingCompl_top_of_isLieAbelian

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ ⁅x, D⁆ ∈ (killingForm R (LieDerivation R L L)).orthogonal (↑(ad R L)).range

Tactic:
exact (rangeAdOrthogonal R L).lie_mem hD

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e ∪ range b.f)
hu : u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ t • u ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| smul t u _ hu =>

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

Goal state before:
pp: case smul
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x : L
t : R
u : L
hx✝ : u ∈ Submodule.span R {x | ∃ u v, ⁅u, v⁆ = x}
hu : (trace R M) (φ u * y) = 0
⊢ (trace R M) (φ (t • u) * y) = 0

Tactic:
| smul t u _ hu =>

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

Goal state before:
pp: R : Type u_1
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        (trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
      ((trace R ↥(genWeightSpace M χ)) (χ y • (toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ LinearMap.id) -
        (trace R ↥(genWeightSpace M χ)) ((χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
LinearMap.comp_id,

Goal state after:
R : Type u_1
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
        (trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
      ((trace R ↥(genWeightSpace M χ)) (χ y • (toEnd R L ↥(genWeightSpace M χ)) x) -
        (trace R ↥(genWeightSpace M χ)) ((χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
⊢ x = 0

Tactic:
suffices ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K H L) by
    simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this
    exact (AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp this
  simp only [LinearMap.mem_ker]
  ext y
  have comm : Commute (toEnd K H L ⟨x, hx⟩) (toEnd K H L y) := by
    rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
  rw [traceForm_apply_apply, ← Module.End.mul_eq_comp, LinearMap.zero_apply]
  exact (LinearMap.isNilpotent_trace_of_isNilpotent (comm.isNilpotent_mul_right hx')).eq_zero

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

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ ((traceForm K L M) x) y = ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (χ x * χ y)

Tactic:
simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy,
    ← traceForm_genWeightSpace_eq K L M _ x y]

Goal state after:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x y : L
hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(genWeightSpace M ⇑χ) ↑(genWeightSpace M ⇑χ)
hds : DirectSum.IsInternal fun i ↦ ↑(genWeightSpace M ⇑i)
⊢ ∑ i, (trace K ↥↑(genWeightSpace M ⇑i)) (((toEnd K L M) x ∘ₗ (toEnd K L M) y).restrict ⋯) =
    ∑ x_1, ((traceForm K L ↥(genWeightSpace M ⇑x_1)) x) y
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⁆
⊢ ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆

Tactic:
← sub_eq_add_neg

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⁆
⊢ ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
⊢ traceForm K L M =
    ∑ χ, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

Tactic:
ext
  rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]
  simp [-LinearMap.coe_smul]

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

Goal state before:
pp: case refine_1
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
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ span K ↑(K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
⊢ ⟨x, hx⟩ ∈ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)

Tactic:
Submodule.span_span

Goal state after:
case refine_1
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
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : x ∈ K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
⊢ ⟨x, hx⟩ ∈ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case h'
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Weight.ker = Weight.ker
⊢ 2 = β (coroot β)

Tactic:
root_apply_coroot hβ

Goal state after:
case h'
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this : Weight.ker = Weight.ker
⊢ 2 = 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
this : (2 * X * T R (↑n + 1)).degree = ↑(n + 2)
⊢ (T R ↑n).degree < (2 * X * T R (↑n + 1)).degree

Tactic:
· rw [ih2, this]; tauto

Goal state after:
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
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
hij : t * P.pairing i j = 2
x : N
h : P.root' j = t • P.root' i
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

Tactic:
simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul]

Goal state after: