mathlib-initiative/mathlib-tactics huggingface dataset:
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) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆
y z : L
hy : y ∈ ⨆ α, rootSpace H α
hz : z ∈ ⨆ α, rootSpace H α
⊢ S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆

Tactic:
induction hy using LieSubmodule.iSup_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✝ : 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' : y ∈ H
hy : S = (ad K L) y
⊢ _root_.IsNilpotent ((ad K L) (x - y))

Tactic:
rwa [map_sub, hSN, hy, add_sub_cancel_right, eq_sub_of_add_eq hSN.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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
⊢ (traceForm K (↥H) L).orthogonal (K ∙ coroot α) = Weight.ker

Tactic:
hyp,

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
⊢ (traceForm K (↥H) L).orthogonal (K ∙ coroot β) = Weight.ker
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
⊢ Weight.ker = Weight.ker

Tactic:
rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]

Goal state after:
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 = (Weight.toLinear K (↥H) L β) (coroot α)

Tactic:
hyp,

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 = (Weight.toLinear K (↥H) L β) (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 : 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 * 1) • e = 2 • e

Tactic:
mul_one,

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 • e = 2 • e
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
degree_U_natCast R m

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : ↑m ≠ -1
⊢ ↑m = ↑((↑m + 1).natAbs - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
degree_U_natCast R m

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
m : ℕ
hn : -↑(m + 1 + 1) ≠ -1
⊢ ↑m = ↑((-↑(m + 1 + 1) + 1).natAbs - 1)
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
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * 1) • α' = coroot α

Tactic:
mul_one,

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
hα : α.IsNonZero
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹) • α' = coroot α
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) +
        ((0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n) +
                derivative (T R ↑n) +
              2 * X * (↑(↑n + 1) * U R (↑n + 1 - 1)) +
            2 * (U R (↑n + 1) - X * U R (↑n + 1 - 1)) +
          ↑n * U R (↑n - 1)) -
      (↑(↑n + 2) * U R (↑n + 2 - 1) +
        (derivative (T R (↑n + 2)) + ↑↑n * U R (↑n - 1) + 2 * X * derivative (T R (↑n + 1)) + 2 * T R (↑n + 1) +
          ↑n * (2 * X * U R ↑n - U R (↑n + 1)))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (-↑n)) = ↑(-↑n) * U R (-↑n - 1)
ih2 : derivative (T R (-↑n + 1)) = ↑(-↑n + 1) * U R (-↑n + 1 - 1)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
h₃ : T R (-↑n) = U R (-↑n) - X * U R (-↑n - 1)
h₁ :
  derivative (T R (-↑n - 1)) = (0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))
⊢ derivative (T R (-↑n - 1)) +
        (derivative (T R (-↑n + 1)) + 2 * X * (↑(-↑n) * U R (-↑n - 1)) +
              ((0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))) +
            2 * (U R (-↑n) - X * U R (-↑n - 1)) +
          (↑n + 1) * (2 * X * U R (-↑n - 1) - U R (-↑n))) -
      (↑(-↑n - 1) * U R (-↑n - 1 - 1) +
        (↑(-↑n + 1) * U R (-↑n + 1 - 1) + 2 * X * derivative (T R (-↑n)) + derivative (T R (-↑n - 1)) + 2 * T R (-↑n) +
          (↑n + 1) * U R (-↑n - 2))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) +
        ((-↑n - 1) * (2 * X * T R (n + 1) - T R n) + (-X ^ 2 + 1) * (↑(n + 1) * U R (n + 1 - 1)) +
          (↑n + 1) * (X * T R (n + 1) - T R (n + 2))) -
      ((↑n + 1) * (T R n - X * T R (n + 1)) +
        ((-↑n - 1) * T R (n + 2) + (-X ^ 2 + 1) * derivative (T R (n + 1)) + (↑n + 1) * ((1 - X ^ 2) * U R n))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  ↑(n + 2) * U R (n + 2 - 1) =
    1 * T R (n + 1) + X * (↑(n + 1) * U R (n + 1 - 1)) -
      ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * derivative (U R n))
h₂ : T R (n + 1) = U R (n + 1) - X * U R (n + 1 - 1)
⊢ (↑n + 1) * T R (n + 1) +
        (1 * T R (n + 1) + X * (↑(n + 1) * U R (n + 1 - 1)) -
            ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * derivative (U R n)) +
          (↑n + 2) * (U R (n + 1) - X * U R (n + 1 - 1))) -
      (X * U R n - (1 - X ^ 2) * derivative (U R n) + (↑(n + 2) * U R (n + 2 - 1) + (↑n + 2) * T R (n + 1))) =
    0

Tactic:
(push_cast; ring_nf)

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

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

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  (0 - ↑2 * X ^ (2 - 1)) * derivative (T R n) + (1 - X ^ 2) * derivative (derivative (T R n)) =
    0 * (T R (n - 1) - X * T R n) + ↑n * (derivative (T R (n - 1)) - (1 * T R n + X * derivative (T R n)))
h₂ :
  (↑(n - 1) + 1) * ↑(n - 1) * T R (n - 1 + 1) =
    ↑(n - 1) * X * derivative (T R (n - 1 + 1)) - (↑(n - 1) + 1) * derivative (T R (n - 1))
⊢ (1 - X ^ 2) * derivative (derivative (T R n)) +
        (0 * (T R (n - 1) - X * T R n) + ↑n * (derivative (T R (n - 1)) - (1 * T R n + X * derivative (T R n))) +
          (↑(n - 1) * X * derivative (T R (n - 1 + 1)) - (↑(n - 1) + 1) * derivative (T R (n - 1)))) -
      (X * derivative (T R n) - ↑n ^ 2 * T R n +
        ((0 - ↑2 * X ^ (2 - 1)) * derivative (T R n) + (1 - X ^ 2) * derivative (derivative (T R n)) +
          (↑(n - 1) + 1) * ↑(n - 1) * T R (n - 1 + 1))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
h :
  (0 + 0) * T R (n + 1) + (↑n + 1) * (↑(n + 1) * U R (n + 1 - 1)) =
    1 * U R n + X * derivative (U R n) -
      ((0 - ↑2 * X ^ (2 - 1)) * derivative (U R n) + (1 - X ^ 2) * derivative (derivative (U R n)))
⊢ (1 - X ^ 2) * derivative (derivative (U R n)) +
        (1 * U R n + X * derivative (U R n) -
          ((0 - ↑2 * X ^ (2 - 1)) * derivative (U R n) + (1 - X ^ 2) * derivative (derivative (U R n)))) -
      (3 * X * derivative (U R n) - (↑n + 2) * ↑n * U R n +
        ((0 + 0) * T R (n + 1) + (↑n + 1) * (↑(n + 1) * U R (n + 1 - 1)))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (T R n) - X ^ 2 * (⇑derivative)^[2] (T R n)) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)

Tactic:
iterate_derivative_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (T R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (T R n)) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (T R n) * X ^ 2) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)

Tactic:
iterate_derivative_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (T R n) * X ^ 2) =
    (⇑derivative)^[k] (X * derivative (T R n)) - (⇑derivative)^[k] (↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)
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
i j : ι
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : AddCommGroup N₂
inst✝¹ : Module R N₂
inst✝ : P.IsRootSystem
e : ι ≃ ι₂
f : M ≃ₗ[R] M₂
g : N ≃ₗ[R] N₂
⊢ span R (range ⇑(RootPairing.map e f g).coroot) = ⊤

Tactic:
simp [Embedding.coe_trans, range_comp, RootPairing.map]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) -
      ((⇑derivative)^[k + 2] (T R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (T R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (T R n)) =
    (⇑derivative)^[k + 1] (T R n) * X + k • (⇑derivative)^[k] (T R n) - ↑(n ^ 2) * (⇑derivative)^[k] (T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) +
        ((⇑derivative)^[k + 1] (T R n) * X + k • (⇑derivative)^[k] (T R n) - ↑(n ^ 2) * (⇑derivative)^[k] (T R n)) -
      ((2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n) +
        ((⇑derivative)^[k + 2] (T R n) -
          ((⇑derivative)^[k + 2] (T R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (T R n) * X +
            (k * (k - 1)) • (⇑derivative)^[k] (T R n)))) =
    0

Tactic:
(push_cast; ring_nf)

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) -
      ((⇑derivative)^[k + 2] (T R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (T R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (T R n)) =
    (⇑derivative)^[k + 1] (T R n) * X + k • (⇑derivative)^[k] (T R n) - ↑(n ^ 2) * (⇑derivative)^[k] (T R n)
⊢ (⇑derivative)^[k] (T R n) * ↑k + (⇑derivative)^[k] (T R n) * ↑k * ↑(k - 1) - (⇑derivative)^[k] (T R n) * ↑k ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (U R n) - X ^ 2 * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
iterate_derivative_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k] (1 * (⇑derivative)^[2] (U R n)) - (⇑derivative)^[k] (X ^ 2 * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (U R n) * X ^ 2) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
iterate_derivative_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (U R n) * X ^ 2) =
    (⇑derivative)^[k] (3 * X * derivative (U R n)) - (⇑derivative)^[k] (↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) -
      ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (U R n)) =
    ↑3 * ((⇑derivative)^[k + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) +
        (↑3 * ((⇑derivative)^[k + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
          ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)) -
      ((2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n) +
        ((⇑derivative)^[k + 2] (U R n) -
          ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
            (k * (k - 1)) • (⇑derivative)^[k] (U R n)))) =
    0

Tactic:
(push_cast; ring_nf)

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) -
      ((⇑derivative)^[k + 2] (U R n) * X ^ 2 + (2 * k) • (⇑derivative)^[k + 1] (U R n) * X +
        (k * (k - 1)) • (⇑derivative)^[k] (U R n)) =
    ↑3 * ((⇑derivative)^[k + 1] (U R n) * X + k • (⇑derivative)^[k] (U R n)) -
      ↑((n + 2) * n) * (⇑derivative)^[k] (U R n)
⊢ (⇑derivative)^[k] (U R n) * ↑k + (⇑derivative)^[k] (U R n) * ↑k * ↑(k - 1) - (⇑derivative)^[k] (U R n) * ↑k ^ 2 = 0
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
p : Submodule R M
v : ↥(span A ↑p)
f : ↑↑p →₀ A
hf : (Finsupp.linearCombination A Subtype.val) f = ↑v
⊢ (tensorToSpan A p) (f.sum fun x a ↦ a ⊗ₜ[R] x) = v

Tactic:
map_finsuppSum,

Goal state after:
case h
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
p : Submodule R M
v : ↥(span A ↑p)
f : ↑↑p →₀ A
hf : (Finsupp.linearCombination A Subtype.val) f = ↑v
⊢ (f.sum fun a b ↦ (tensorToSpan A p) (b ⊗ₜ[R] a)) = v
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
x : R
h :
  (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (T R n)) =
    (2 * ↑k + 1) * x * eval x ((⇑derivative)^[k + 1] (T R n)) - (↑n ^ 2 - ↑k ^ 2) * eval x ((⇑derivative)^[k] (T R n))
⊢ (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (T R n)) +
        ((2 * ↑k + 1) * x * eval x ((⇑derivative)^[k + 1] (T R n)) -
          (↑n ^ 2 - ↑k ^ 2) * eval x ((⇑derivative)^[k] (T R n))) -
      ((2 * ↑k + 1) * x * eval x ((⇑derivative)^[k + 1] (T R n)) -
          (↑n ^ 2 - ↑k ^ 2) * eval x ((⇑derivative)^[k] (T R n)) +
        (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (T R n))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
x : R
h :
  (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (U R n)) =
    (2 * ↑k + 3) * x * eval x ((⇑derivative)^[k + 1] (U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval x ((⇑derivative)^[k] (U R n))
⊢ (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (U R n)) +
        ((2 * ↑k + 3) * x * eval x ((⇑derivative)^[k + 1] (U R n)) -
          ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval x ((⇑derivative)^[k] (U R n))) -
      ((2 * ↑k + 3) * x * eval x ((⇑derivative)^[k + 1] (U R n)) -
          ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval x ((⇑derivative)^[k] (U R n)) +
        (1 - x ^ 2) * eval x ((⇑derivative)^[k + 2] (U R n))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (T R n)) = -((↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (T R n)) + -((↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))) -
      (-(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n)) + eval 0 ((⇑derivative)^[k + 2] (T R n))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (U R n)) = -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) + -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))) -
      (-((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)) + eval 0 ((⇑derivative)^[k + 2] (U R n))) =
    0

Tactic:
(push_cast; ring_nf)

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 1 = C R (m + 1) + C R (m - 1)

Tactic:
C_add_one,

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 1 = X * C R m - C R (m - 1) + C R (m - 1)
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ comap (factorPow I le) (map (mk (I ^ a)) I) = map (mk (I ^ b)) I

Tactic:
apply Ideal.map_mk_comap_factor

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
a b : ℕ
apos : 0 < a
le : a ≤ b
⊢ I ^ a ≤ I