mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
⊢ ⨆ x, rootSpace H ↑(e x) = ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i))

Tactic:
;

Goal state after:
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
⊢ ⨆ x, rootSpace H ↑(e x) = ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ n < n + 1 + 1

Tactic:
;

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ n < n + 1 + 1
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))

Tactic:
;

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))
⊢ eval (-x) (U R (↑n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ χ ∈ s, rootSpace H χ = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
;

Goal state after:
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ χ ∈ s, rootSpace H χ = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
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))
⊢ 2 * x * ((-1) ^ n * eval x (U R (↑n + 1))) - (-1) ^ n * eval x (U R ↑n) =
    (-1) ^ n * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

Tactic:
;

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))
⊢ 2 * x * ((-1) ^ n * eval x (U R (↑n + 1))) - (-1) ^ n * eval x (U R ↑n) =
    (-1) ^ n * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℤ
inst✝¹ : IsDomain R
inst✝ : NeZero 2
h : n ≠ -1
⊢ U R n ≠ 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : ℤ
inst✝¹ : IsDomain R
inst✝ : NeZero 2
h : n ≠ -1
⊢ U R n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ 4 * X ^ 2 - 1 = X * (2 * X) + (2 * X ^ 2 - 1)

Tactic:
;

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 4 * X ^ 2 - 1 = X * (2 * X) + (2 * X ^ 2 - 1)
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ x, rootSpace H ↑(e x) = ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i))

Tactic:
;

Goal state after:
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ x, rootSpace H ↑(e x) = ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i))
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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
hv : v ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i)) = ⨆ x, LieModule.genWeightSpace L ↑(e x)

Tactic:
;

Goal state after:
ι : 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 u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
hv : v ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ x, rootSpace H (∑ i, ↑x i • ⇑(b.baseSupp i)) = ⨆ x, LieModule.genWeightSpace L ↑(e x)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
;

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 • T R 1 ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ U R (↑n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))

Tactic:
;

Goal state after:
case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ U R (↑n + 2) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R (↑n + 2) + U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))

Tactic:
;

Goal state after:
case more
R : Type u_1
inst✝ : CommRing R
n : ℕ
h₀ : U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 n)
a✝ : U R ↑(n + 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 1))
⊢ 2 • T R (↑n + 2) + U R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-1 + -↑k + 2) + (X * C R (-↑k) - C R (-↑k + 1)) - X * C R (-↑k) = 0

Tactic:
;

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-1 + -↑k + 2) + (X * C R (-↑k) - C R (-↑k + 1)) - X * C R (-↑k) = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R (-↑n.natAbs)

Tactic:
;

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ C R ↑n.natAbs = C R (-↑n.natAbs)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
;

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (↑n + 1)) = 2
ih2 : eval 2 (C R ↑n) = 2
⊢ 2 * 2 - 2 = 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
;

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (C R (-↑n)) = 2
ih2 : eval 2 (C R (-↑n + 1)) = 2
⊢ 2 * 2 - 2 = 2
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-1 + -↑k + 2) + (X * S R (-↑k) - S R (-↑k + 1)) - X * S R (-↑k) = 0

Tactic:
;

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-1 + -↑k + 2) + (X * S R (-↑k) - S R (-↑k + 1)) - X * S R (-↑k) = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ 1 + X ^ 2 - X * X = 1

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ 1 + X ^ 2 - X * X = 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 * (X ^ 2 - 1) = X * X + (X ^ 2 - 2)

Tactic:
;

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 * (X ^ 2 - 1) = X * X + (X ^ 2 - 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 * S R (1 + 1) = X * S R 1 + C R (1 + 1)

Tactic:
simp [S_two, C_two]; ring

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 + 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:
;

Goal state after:
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
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:
;

Goal state after:
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
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 x✝ : ι
⊢ (⇑(P.reflectionPerm i))^[2] x✝ = id x✝

Tactic:
;

Goal state after:
ι : 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 x✝ : ι
⊢ (⇑(P.reflectionPerm i))^[2] x✝ = id x✝
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 : ι
x : M
⊢ (P.reflection ((P.reflectionPerm j) i)) x = (P.reflection j * P.reflection i * P.reflection j) x

Tactic:
;

Goal state after:
ι : 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 : ι
x : M
⊢ (P.reflection ((P.reflectionPerm j) i)) x = (P.reflection j * P.reflection i * P.reflection j) x
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 : ι
x : M
⊢ x -
      ((P.toLinearMap x) (P.coroot i) - P.pairing j i * (P.toLinearMap x) (P.coroot j)) •
        (P.root i - P.pairing i j • P.root j) =
    x - (P.toLinearMap x) (P.coroot j) • P.root j -
        ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) • P.root i -
      ((P.toLinearMap x) (P.coroot j) - (P.toLinearMap x) (P.coroot j) * 2 -
          ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) * P.pairing i j) •
        P.root j

Tactic:
;

Goal state after:
ι : 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 : ι
x : M
⊢ x -
      ((P.toLinearMap x) (P.coroot i) - P.pairing j i * (P.toLinearMap x) (P.coroot j)) •
        (P.root i - P.pairing i j • P.root j) =
    x - (P.toLinearMap x) (P.coroot j) • P.root j -
        ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) • P.root i -
      ((P.toLinearMap x) (P.coroot j) - (P.toLinearMap x) (P.coroot j) * 2 -
          ((P.toLinearMap x) (P.coroot i) - (P.toLinearMap x) (P.coroot j) * P.pairing j i) * P.pairing i j) •
        P.root j
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ ↑↑n • U R (↑n - 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)

Tactic:
;

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : n ≠ 0
⊢ ↑↑n • U R (↑n - 1) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Ico 0 n)
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: 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
m : ℤ
t : R
ht : t = f y * g x - 2
⊢ ((reflection hf * reflection hg) ^ m) x =
    (Polynomial.eval t (S R m) + Polynomial.eval t (S R (m - 1))) • x + (Polynomial.eval t (S R (m - 1)) * -g x) • y

Tactic:
by
  /- Even though this is a special case of `Module.reflection_mul_reflection_zpow_apply`, it is
  easier to prove it from scratch. -/
  have S_eval_t_sub_two (k : ℤ) :
      (S R (k - 2)).eval t = (f y * g x - 2) * (S R (k - 1)).eval t - (S R k).eval t := by
    simp [S_sub_two, ht]
  induction m with
  | zero => simp
  | succ m ih =>
    -- Apply the inductive hypothesis.
    rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (m + 1)
    · ring_nf
  | pred m ih =>
    -- Apply the inductive hypothesis.
    rw [sub_eq_add_neg (-m : ℤ) 1, add_comm (-m : ℤ) (-1), zpow_add, zpow_neg_one, mul_inv_rev,
      reflection_inv, reflection_inv, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- Equate coefficients of `x` and `y`.
    match_scalars
    · linear_combination (norm := ring_nf) -S_eval_t_sub_two (-m)
    · linear_combination (norm := ring_nf) g x * S_eval_t_sub_two (-m)

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:
;

Goal state after:
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
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x x✝ : N
⊢ (P.root' j) x✝ = (t • P.root' i) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x x✝ : N
⊢ (P.root' j) x✝ = (t • P.root' i) x✝
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f 0 = 2
hf₂ : MapsTo (⇑(preReflection 0 f)) Φ Φ
hg₁ : g 0 = 2
hg₂ : MapsTo (⇑(preReflection 0 g)) Φ Φ
⊢ False

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f 0 = 2
hf₂ : MapsTo (⇑(preReflection 0 f)) Φ Φ
hg₁ : g 0 = 2
hg₂ : MapsTo (⇑(preReflection 0 g)) Φ Φ
⊢ False