mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
simp

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

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

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

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
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
n : ↑{n | n ≠ 0}
x✝ : ↥H
⊢ (∑ i, ↑n i • ⇑(b.baseSupp i)) x✝ = (∑ i, ↑n i • b.baseSupp i) x✝

Tactic:
simp

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

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

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

Tactic:
simp

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1
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:
simp

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

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

Tactic:
simp

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ -2 = -1 + -1
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 0 (U R (2 * n)) = ↑↑n.negOnePow

Tactic:
simp

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

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
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
⊢ Bijective fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩

Tactic:
refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (U R (-1)).degree = ⊥

Tactic:
simp

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

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

Tactic:
simp

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

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (U R (-1)).natDegree = (-1 + 1).natAbs - 1

Tactic:
simp

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

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

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

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

Tactic:
simp

Goal state after:
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) 2 * eval (-x) X * (↑↑(-(↑n).negOnePow) * eval x (U R (↑n + 1))) - ↑↑(↑n).negOnePow * eval x (U R ↑n) =
    ↑↑((↑n).negOnePow * 1) * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

Tactic:
simp

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

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ U R ↑1 = 2 * T R 1

Tactic:
simp

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

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

Tactic:
rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]

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: R : Type u_1
inst✝ : CommRing R
⊢ 1 ∈ Set.Icc 0 1 ∧ (fun m ↦ T R ↑m) 1 = T R 1

Tactic:
simp

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

Goal state before:
pp: 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))
⊢ n + 2 ∈ Set.Icc 0 (n + 2) ∧ (fun m ↦ T R ↑m) (n + 2) = T R ↑(n + 2)

Tactic:
simp

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
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
⊢ (∃ c₁ c₂ c₃,
      x = c₁ • Classical.choose he + c₂ • Classical.choose hf + c₃ • ⁅Classical.choose he, Classical.choose hf⁆) ↔
    ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
hcf,

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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
⊢ (∃ c₁ c₂ c₃, x = c₁ • Classical.choose he + c₂ • cf • f + c₃ • ⁅Classical.choose he, cf • f⁆) ↔
    ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
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:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (C R 0).comp (2 * X) = 2 * T R 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
⊢ iSupIndep ![rootSpace H 0, U, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]

Tactic:
set V := ⨆ (n : ι → ℕ) (_ : n ≠ 0), rootSpace H (∑ i, n i • b.baseSupp i) with hV

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
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
⊢ iSupIndep ![rootSpace H 0, U, V]
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ eval (-2) (C R 1) = 2 * ↑↑(Int.negOnePow 1)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ S R (-1 - 1) = -S R (1 - 1)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (S R 0).comp (2 * X) = U R 0

Tactic:
simp

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

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

Tactic:
simp

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
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ coroot α ∈ ↑(corootSpace ⇑α)

Tactic:
simp

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

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

Tactic:
simp

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 zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (T R 0) = T R' 0

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (T R 1) = T R' 1

Tactic:
simp

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
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
⊢ ((reflection hf * reflection hg) ^ 0) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (0 - 1))) • x + (Polynomial.eval t (S R (0 - 1)) * -g x) • y

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (U R 0) = U R' 0

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (U R 1) = U R' 1

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (C R 0) = C R' 0

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (C R 1) = C R' 1

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (S R 0) = S R' 0

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (S R 1) = S R' 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
⊢ derivative (T R 1) = ↑1 * U R (1 - 1)

Tactic:
simp

Goal state after:
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 : ι
⊢ (P.flip (P.coroot i)) (P.root j) = P.pairing j i

Tactic:
simp

Goal state after:
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 : ι
⊢ (P.flip (P.coroot i)) (P.root i) = 2

Tactic:
simp

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ n ∈ Set.Icc 0 (n - 0) ∧ (fun m ↦ T R ↑m) n = T R ↑n

Tactic:
simp

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

Goal state before:
pp: case e'_4
R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
this :
  Submodule.span ℕ ((fun m ↦ derivative (T R ↑m)) '' Set.Icc 0 (n - k)) ≤
    Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1)))
⊢ (fun m ↦ derivative (T R ↑m)) '' Set.Icc 0 (n - k) = ⇑(↑ℕ derivative) '' (fun m ↦ T R ↑m) '' Set.Icc 0 (n - k)

Tactic:
simp [Set.image]

Goal state after:
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 : ι
⊢ P.root ((P.reflectionPerm i) i) = -P.root i

Tactic:
simp

Goal state after:
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
⊢ t * P.pairing i j = 2

Tactic:
simpa using ((P.coroot' j).congr_arg h).symm

Goal state after:
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
⊢ (P.root' i) (P.coroot i) = 2

Tactic:
simp

Goal state after:
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
⊢ t • P.coroot j = P.coroot i

Tactic:
refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i)
    (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_
    (P.mapsTo_coreflection_coroot i) (mem_range_self i)

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
⊢ MapsTo (⇑(preReflection (t • P.coroot j) (P.root' i))) (range ⇑P.coroot) (range ⇑P.coroot)
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
⊢ MapsTo (⇑(preReflection (t • P.coroot j) (P.root' i))) (range ⇑P.coroot) (range ⇑P.coroot)

Tactic:
convert! P.mapsTo_coreflection_coroot j

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
⊢ ⇑(preReflection (t • P.coroot j) (P.root' i)) = ⇑(P.coreflection j)
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ ↑(u ^ 0) = LinearMap.id + ↑0 • LinearMap.smulRight (f - g) x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case refine_1.zero
ι : 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 : ι
h : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.reflection i) 0 = (P.reflection j) 0

Tactic:
simp

Goal state after: