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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : ⁅↑j, z⁆ = 0 ∧ ⁅↑j, y + z⁆ = 0
⊢ ⁅j, ⟨y, hy⟩⁆ = 0

Tactic:
lie_add,

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
this : ⁅↑j, z⁆ = 0 ∧ ⁅↑j, y⁆ + ⁅↑j, z⁆ = 0
⊢ ⁅j, ⟨y, hy⟩⁆ = 0
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
⊢ (trace R ↥p) (f.restrict hf') = (trace R M) f

Tactic:
by
  let ι := Module.Free.ChooseBasisIndex R M
  obtain ⟨n, snf⟩ := p.smithNormalForm (Module.Free.chooseBasis R M)
  rw [trace_eq_matrix_trace R snf.bM, trace_eq_matrix_trace R snf.bN]
  set A : Matrix (Fin n) (Fin n) R := toMatrix snf.bN snf.bN (f.restrict hf')
  set B : Matrix ι ι R := toMatrix snf.bM snf.bM f
  have aux : ∀ i, B i i ≠ 0 → i ∈ Set.range snf.f := fun i hi ↦ by
    contrapose hi; exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi
  change ∑ i, A i i = ∑ i, B i i
  rw [← Finset.sum_filter_of_ne (p := fun j ↦ j ∈ Set.range snf.f) (by simpa using aux)]
  simp [A, B, hf, Finset.sum_image snf.f.injective.injOn]

Goal state after:
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 : ℕ
⊢ (map (↑(toSplittingField s)) (subProdXSubC f)).coeff n = 0

Tactic:
subProdXSubC,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(toSplittingField s))
          (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f - ∏ i, (X - C (MvPolynomial.X ⟨f, i⟩)))).coeff
      n =
    0
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
⊢ (killingForm R L).Nondegenerate

Tactic:
refine (LieModule.traceForm_isSymm R L L).isRefl.nondegenerate_iff_separatingLeft.mpr ?_

Goal state after:
R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ LinearMap.SeparatingLeft (LieModule.traceForm R L L)
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ ⨆ μ, f.eigenspace μ = ⊤

Tactic:
simpa only [(isFinitelySemisimple_iff_isSemisimple.mpr hf).maxGenEigenspace_eq_eigenspace] using
    iSup_maxGenEigenspace_eq_top f

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.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✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
h : rootSpace H 0 ⊔ LieModule.posFittingComp R (↥H) L = ⊤
⊢ Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)

Tactic:
← LieSubmodule.toSubmodule_inj,

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : IsKilling R L
inst✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
h : ↑(rootSpace H 0 ⊔ LieModule.posFittingComp R (↥H) L) = ↑⊤
⊢ Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)
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✝ : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
⊢ x ∈ LinearMap.ker (killingForm K L)

Tactic:
by
  rw [LinearMap.mem_ker]
  ext y
  have hy : y ∈ ⨆ β, rootSpace H β := by simp [iSup_genWeightSpace_eq_top K H L]
  induction hy using LieSubmodule.iSup_induction' with
  | mem β y hy =>
    by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
  | zero => simp
  | add => simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : (s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
⊢ g i = 0

Tactic:
have le_sup := Finset.le_sup hi (f := fun i ↦ (g i • S i).degree)

Goal state after:
case pos
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : (s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
le_sup : (g i • ↑S i).degree ≤ s.sup fun i ↦ (g i • ↑S i).degree
⊢ g i = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case hf
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ ⨆ μ, ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace μ = ⊤

pp: case hg
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ ∀ (μ : A),
    (trace A ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace μ))
        (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) =
      0

pp: case h_comm
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ Commute ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z))

Tactic:
· exact IsTriangularizable.maxGenEigenspace_eq_top (1 ⊗ₜ[R] x)

Goal state after:
case hg
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ ∀ (μ : A),
    (trace A ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace μ))
        (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) =
      0

case h_comm
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ Commute ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z))
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 : L
χ : Weight K L M
x✝ : χ ∈ Finset.univ
⊢ finrank K ↥(genWeightSpace M ⇑χ) • χ x • Weight.toLinear K L M χ ∈ span K (range (Weight.toLinear K L M))

Tactic:
← Nat.cast_smul_eq_nsmul K

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 : L
χ : Weight K L M
x✝ : χ ∈ Finset.univ
⊢ ↑(finrank K ↥(genWeightSpace M ⇑χ)) • χ x • Weight.toLinear K L M χ ∈ span K (range (Weight.toLinear K L M))
Module: Mathlib.Algebra.Lie.Weights.Killing

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

Tactic:
this,

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
this : h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ α h ≠ 0

Tactic:
this,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
this : h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ α (((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ≠ 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
inst✝ : Fintype ι
i : ι
x : L
t : R
u : L
hu : u ∈ Submodule.span R (range b.h)
hv' : ∀ (hx : u ∈ H), (b.baseSupp i) ⟨u, hx⟩ • b.e i = ⁅u, b.e i⁆
hx : t • u ∈ H
⊢ (b.baseSupp i) ⟨t • u, hx⟩ • b.e i = ⁅t • u, b.e i⁆

Tactic:
| smul t u hu hv' =>

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ (2 * (α h)⁻¹) • ⁅⁅e, f'⁆, e⁆ = 2 • e

Tactic:
this,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ (2 * (α h)⁻¹) • α h • e = 2 • e
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
this : 2 • e = α h • e
⊢ α h = 2

Tactic:
exact smul_left_injective K ht.e_ne_zero this.symm

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
s : K
hs : s • h = coroot α
⊢ h = coroot α

Tactic:
replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
s : K
hs : s • h = coroot α
this : s = 1
⊢ h = coroot α
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
s : K
hs : s • h = coroot α
this : s = 1
⊢ h = coroot α

Tactic:
this,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
s : K
hs : 1 • h = coroot α
this : s = 1
⊢ h = coroot α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ U R ↑1 ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 1)

Tactic:
rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]; norm_cast
    exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ (X * C R (↑n + 1)).comp (2 * X) - (C R ↑n).comp (2 * X) = 2 * (2 * X * T R (↑n + 1) - T R ↑n)

Tactic:
mul_comp,

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ X.comp (2 * X) * (C R (↑n + 1)).comp (2 * X) - (C R ↑n).comp (2 * X) = 2 * (2 * X * T R (↑n + 1) - T R ↑n)
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✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
x✝ : ∃ c₁ c₂ c₃, x = c₁ • ce • e + c₂ • cf • f + c₃ • ⁅ce • e, cf • f⁆
c₁ c₂ c₃ : K
hx : x = c₁ • ce • e + c₂ • cf • f + c₃ • ⁅ce • e, cf • f⁆
⊢ x = (c₁ * ce) • e + (c₂ * cf) • f + (c₃ * cf * ce) • ⁅e, f⁆

Tactic:
simp [hx, mul_smul]

Goal state after:
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
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
      ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]

Tactic:
let := b.isLieAbelian_cartan
  intro i
  fin_cases i
  · exact toLieSubmodule_le_rootSpace_zero R L H
  · exact b.borelLower_le_biSup
  · exact b.borelUpper_le_biSup

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ (X * C R (-↑n)).comp (2 * X) - (C R (-↑n + 1)).comp (2 * X) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 1))

Tactic:
mul_comp,

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ X.comp (2 * X) * (C R (-↑n)).comp (2 * X) - (C R (-↑n + 1)).comp (2 * X) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 1))
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ c₁_1 c₂_1 c₃_1, ⁅↑h, c₁ • e + c₂ • f + c₃ • ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆

Tactic:
lie_add,

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ c₁_1 c₂_1 c₃_1, ⁅↑h, c₁ • e + c₂ • f⁆ + ⁅↑h, c₃ • ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ c₁_1 c₂_1 c₃_1, ⁅↑h, c₁ • e + c₂ • f⁆ + ⁅↑h, c₃ • ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆

Tactic:
lie_add,

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ∃ c₁_1 c₂_1 c₃_1, ⁅↑h, c₁ • e⁆ + ⁅↑h, c₂ • f⁆ + ⁅↑h, c₃ • ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆