mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T ∈ S

Tactic:
suffices sSup T = a from this ▸ hT haT

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T = a
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
a✝ : ∀ (y : LieIdeal K L), InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ finrank K ↥x) y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this✝ : I ≤ J ⊔ J' ⊓ I
this : ¬I ≤ J'
⊢ ↑(orthogonal Φ hΦ_inv J ⊓ I) < ↑I

Tactic:
simpa

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

Goal state before:
pp: case inr
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
x : L
hx : x ∈ I
⊢ x ∈ K

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y ∈ id J, ∃ z ∈ K, y + z = x := by
    rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]
    exact hI.le hx

Goal state after:
case inr
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
⊢ y + z ∈ K
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible f.factor

Tactic:
factor

Goal state after:
K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)
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
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
i : ι
hi : i ∉ Set.range ⇑snf.f
⊢ B i i = 0

Tactic:
exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ -↑p < 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ ↑q > 0

Tactic:
simpa

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
this : H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤
⊢ iSup ![H.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
simpa

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

Goal state before:
pp: case convert_2
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    ∑ k ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥(genWeightSpace M (k • α + χ))) ((toEnd R ↥H ↥(genWeightSpace M (k • α + χ))) x)

Tactic:
trace_toEnd_genWeightSpace,

Goal state after:
case convert_2
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    ∑ x_1 ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (x_1 • α + χ)) • (x_1 • α + χ) x
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
x y z : L
⊢ ((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) ⁅y, x⁆) z

Tactic:
by rw [← lie_skew x y, map_neg, LinearMap.neg_apply]

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

Goal state before:
pp: case mem
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 a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ 0 c = 0

Tactic:
LinearMap.zero_apply

Goal state after:
case mem
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 a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ 0 = 0
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) -
        χ x • (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) y) -
      (χ y • (trace R ↥(genWeightSpace M χ)) ((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)

Tactic:
trace_toEnd_genWeightSpace,

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) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • (trace R ↥(genWeightSpace M χ)) ((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.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) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • (trace R ↥(genWeightSpace M χ)) ((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)

Tactic:
trace_toEnd_genWeightSpace,

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) -
        χ x • finrank R ↥(genWeightSpace M χ) • χ y -
      (χ y • finrank R ↥(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.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ n < m

Tactic:
Polynomial.mem_degreeLT

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P.degree < ↑m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ n < m
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:
rootSpace_zero_eq R L H,

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 : ↑H.toLieSubmodule ⊔ ↑(LieModule.posFittingComp R (↥H) L) = ⊤
⊢ Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
this : tail.degree < ↑m
⊢ P - head ∈ degreeLT R m

Tactic:
Polynomial.mem_degreeLT

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
this : tail.degree < ↑m
⊢ (P - head).degree < ↑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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
y : ↥H
comm : Commute ((toEnd K (↥H) L) ⟨x, hx⟩) ((toEnd K (↥H) L) y)
⊢ (LinearMap.trace K L) ((toEnd K (↥H) L) ⟨x, hx⟩ * (toEnd K (↥H) L) y) = 0 y

Tactic:
LinearMap.zero_apply

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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
y : ↥H
comm : Commute ((toEnd K (↥H) L) ⟨x, hx⟩) ((toEnd K (↥H) L) y)
⊢ (LinearMap.trace K L) ((toEnd K (↥H) L) ⟨x, hx⟩ * (toEnd K (↥H) L) y) = 0
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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
x : L
⊢ (trace R M) (φ z ∘ₗ φ x) = 0 x

Tactic:
LinearMap.zero_apply

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✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
x : L
⊢ (trace R M) (φ z ∘ₗ φ x) = 0
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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ (α + β) x' • ⁅y, z⁆ = α x' • ⁅y, z⁆ + β x' • ⁅y, z⁆

Tactic:
← add_smul,

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
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ (α + β) x' • ⁅y, z⁆ = (α x' + β x') • ⁅y, z⁆
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n + 1) = 2 * X * T R n - T R (n - 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n - 1) = 2 * X * T R n - T R (n + 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
this : 2 * X - X = X
⊢ 2 * X * T R (-↑0) - T R (-↑0 + 1) = X

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ T R (-1) = X

Tactic:
change T R (Int.negSucc 0) = X
  rw [T]
  suffices 2 * X - X = X by simpa
  ring

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

Goal state before:
pp: case mem
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
x y z : ↥H
u : L
hu : u ∈ rootSpace H ⇑α
v : L
huv : ⁅u, v⁆ = ↑z
hx : α x = 0
⊢ 0 v = 0

Tactic:
LinearMap.zero_apply

Goal state after:
case mem
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
x y z : ↥H
u : L
hu : u ∈ rootSpace H ⇑α
v : L
huv : ⁅u, v⁆ = ↑z
hx : α x = 0
⊢ 0 = 0
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α : α.IsZero
⊢ coroot α = 0

Tactic:
simpa

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
x : L
hx : x ∈ lieSpan R L (range b.e ∪ range b.f)
⊢ x ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
induction hx using lieSpan_induction with

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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
⊢ (traceForm K (↥H) L).orthogonal (K ∙ coroot β) = Weight.ker

Tactic:
orthogonal_span_coroot_eq_ker

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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
⊢ Weight.ker = Weight.ker
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ eval (-x) (U R ↑(n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))

Tactic:
· push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))
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
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
⊢ (-α).IsNonZero

Tactic:
simpa

Goal state after: