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

Goal state before:
pp: case zero
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
hm : ⁅h, m⁆ = μ • m
⊢ ⁅h, ((toEnd R L M) e ^ 0) m⁆ = (μ + 2 * ↑0) • ((toEnd R L M) e ^ 0) m

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
⊢ ((toEnd R L M) x ^ 0) m ∈ lowerCentralSeries R L M 0

Tactic:
| zero =>

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

Goal state before:
pp: case mem.zero
ι : 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
i : ι
⊢ ⁅0, b.e i⁆ ∈ lieSpan R L (range b.e)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
⊢ ⁅x, 0⁆ ∈ lieSpan R L (range b.e)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
⊢ ⁅b.e i, 0⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ {a | IsAtom a} ⊆ S

Tactic:
intro a

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ a ∈ {a | IsAtom a} → a ∈ S
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ B.orthogonal W = ⊤ ↔ W = ⊥

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).inf_eq_bot
  rwa [h, inf_top_eq] at this

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

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
⊢ W = ⊤

Tactic:
by
  have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top
  rwa [b₃, sup_bot_eq] at this

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

Goal state before:
pp: case zero
ι : 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
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅0, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ ∀ (a : α), (filter (fun a_1 ↦ a = a_1.1) s.val).card ≤ count a m

Tactic:
rintro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
⊢ (filter (fun a_1 ↦ a = a_1.1) s.val).card ≤ count a m
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst = v
h : ¬↑x.snd = count v m
⊢ ↑x.snd < count v m

Tactic:
apply lt_of_le_of_ne (Nat.le_of_lt_add_one _) h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst = v
h : ¬↑x.snd = count v m
⊢ ↑x.snd < count v m + 1
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: case mp
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
h : center R L = ⊤
hc : ⊤ = ⊥
⊢ Subsingleton L

Tactic:
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_top_eq_bot hc)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: case h.zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ (f ^ S.sup g) 0 = 0 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y : M
⊢ ⁅x, 0⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
⊢ 0 ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) 0) = 0

Tactic:
| zero =>

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
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 χ ≠ ⊥
⊢ ∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Tactic:
obtain ⟨p, hp₀, q, hq₀, hp, hq⟩ := exists₂_genWeightSpace_smul_add_eq_bot M α χ hα
  let a := ∑ i ∈ Finset.Ioo p q, finrank R (genWeightSpace M (i • α + χ)) • i
  let b := ∑ i ∈ Finset.Ioo p q, finrank R (genWeightSpace M (i • α + χ))
  have hb : 0 < b := by
    replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]
    refine Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩
    rw [zero_smul, zero_add]
    exact finrank_pos
  refine ⟨a, b, Int.natCast_pos.mpr hb, fun x hx ↦ ?_⟩
  let N : ℤ → Submodule R M := fun k ↦ genWeightSpace M (k • α + χ)
  have h₁ : iSupIndep fun (i : Finset.Ioo p q) ↦ N i := by
    rw [LieSubmodule.iSupIndep_toSubmodule]
    refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_
    exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij
  have h₂ : ∀ i, MapsTo (toEnd R H M x) ↑(N i) ↑(N i) := fun _ _ ↦ LieSubmodule.lie_mem _
  have h₃ : genWeightSpaceChain M α χ p q = ⨆ i ∈ Finset.Ioo p q, N i := by
    simp_rw [N, genWeightSpaceChain_def', LieSubmodule.iSup_toSubmodule]
  rw [← trace_toEnd_genWeightSpaceChain_eq_zero M α χ p q hp hq hx,
    ← LieSubmodule.toEnd_restrict_eq_toEnd]
  -- The lines below illustrate the cost of treating `LieSubmodule` as both a
  -- `Submodule` and a `LieSubmodule` simultaneously.
  #adaptation_note /-- 2025-06-18 (https://github.com/leanprover/lean4/issues/8804).
    The `erw` causes a kernel timeout if there is no `subst`. -/
  subst a b N
  erw [LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃]
  simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]
  convert_to! _ =
    ∑ k ∈ Finset.Ioo p q, (LinearMap.trace R { x // x ∈ (genWeightSpace M (k • α + χ)) })
      ((toEnd R { x // x ∈ H } { x // x ∈ genWeightSpace M (k • α + χ) }) x)
  simp_rw [trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add,
    ← smul_assoc, Finset.sum_add_distrib, ← Finset.sum_smul, natCast_zsmul]

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

Goal state before:
pp: case zero
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
⊢ (trace R M) (φ 0 * y) = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ ∃ n, ((toEnd K L M) x ^ n) 0 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 : L
hx : x ∈ ⊤.lcs L 0
hy : y ∈ LieSubmodule.ucs 0 ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
N : Type u_5
N' : Type u_6
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup M'
inst✝⁶ : AddCommGroup N'
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R N
inst✝¹ : Module R N'
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
eM : M' ≃ₗ[R] M
eN : N' ≃ₗ[R] N
q : M' →ₗ[R] N' →ₗ[R] R
H : q.compl₁₂ ↑eM.symm ↑eN.symm = p
⊢ q = p.compl₁₂ ↑eM ↑eN

Tactic:
subst H; ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
V : Submodule R N
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact eq_top_of_isCompl_bot <| by simpa using h.isCompl_right
  · rw [h]
    exact
      { isCompl_left := by simpa using isCompl_top_bot
        isCompl_right := by simpa using isCompl_top_bot }

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

Goal state before:
pp: case zero
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
B : LinearMap.BilinForm R M
hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
⊢ ∀ (m n : M), (B m) ((φ x ^ 0) n) = (-1) ^ 0 • (B ((φ x ^ 0) m)) n

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
y : L
⊢ ((killingForm K L) x) 0 = 0 0

Tactic:
| zero =>

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

Goal state before:
pp: case mem.zero
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) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆
y✝ z : L
α : ↥H → K
y : L
hy : y ∈ rootSpace H α
⊢ S ⁅y, 0⁆ = ⁅S y, 0⁆ + ⁅y, S 0⁆

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆
y z : L
hz : z ∈ ⨆ α, rootSpace H α
⊢ S ⁅0, z⁆ = ⁅S 0, z⁆ + ⁅0, S z⁆

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
⊢ ((reflection hf * reflection hg) ^ 0) z =
    z +
        (Polynomial.eval t (S R ((↑0 - 2) / 2)) *
            (Polynomial.eval t (S R ((↑0 - 1) / 2)) + Polynomial.eval t (S R ((↑0 - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑0 - 1) / 2)) *
          (Polynomial.eval t (S R (↑0 / 2)) + Polynomial.eval t (S R ((↑0 - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ), motive (-n) → motive n
h₀ : motive (-↑0)
h₁ : motive (-↑0 + 1)
⊢ motive (-↑0 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ T R (-0) = T R 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 : ↥H
hx : x ∈ Weight.ker
⊢ ((traceForm K (↥H) L) x) 0 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (T R 0) = 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval (-1) (T R 0) = ↑↑(Int.negOnePow 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 0 (T R 0) = ↑(if Even 0 then ↑(0 / 2).negOnePow else 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (T R 0).degree = ↑(Int.natAbs 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
hx : 0 ∈ H
⊢ (b.baseSupp i) ⟨0, hx⟩ • b.e i = ⁅0, b.e i⁆

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (T R 0).leadingCoeff = 2 ^ (Int.natAbs 0 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
x : R
⊢ eval (-x) (T R 0) = ↑↑(Int.negOnePow 0) * eval x (T R 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x : L
⊢ 0 ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ U R (-0 - 1) = -U R (0 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (U R 0) = ↑0 + 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval (-1) (U R 0) = ↑↑(Int.negOnePow 0) * (↑0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 0 (U R 0) = ↑(if Even 0 then ↑(0 / 2).negOnePow else 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (U R ↑0).degree = ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
hn : -↑0 ≠ -1
⊢ (U R (↑0 - 2)).degree = ↑((-↑0 + 1).natAbs - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
hn : -↑(0 + 1) ≠ -1
⊢ (U R (↑(0 + 1) - 2)).degree = ↑((-↑(0 + 1) + 1).natAbs - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
⊢ (U R ↑0).leadingCoeff = 2 ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
x : R
⊢ eval (-x) (U R ↑0) = ↑↑(↑0).negOnePow * eval x (U R ↑0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ U R (0 + 1) = X * U R 0 + T R (0 + 1)

Tactic:
| zero =>

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
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 (-⇑α)
c : K
hc : c • ⟨e, hte⟩ = ⟨he.choose, ⋯⟩
⊢ ∃ c, he.choose = c • e

Tactic:
exact ⟨c, by simpa using hc.symm⟩

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

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

Tactic:
| zero =>

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
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
c : K
hc : c • ⟨f, htf⟩ = ⟨hf.choose, ⋯⟩
⊢ ∃ c, hf.choose = c • f

Tactic:
exact ⟨c, by simpa using hc.symm⟩

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ C R (-0) = C R 0

Tactic:
| zero =>

Goal state after: