mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case a.inl
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
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((0 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((0 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (0 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (0 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((0 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((0 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (0 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (0 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

Tactic:
ring_nf

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case a.inr
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
m : ℕ
k : ℤ := ↑m / 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R (k - 2)) =
      (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) - Polynomial.eval (f y * g x - 2) (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval (f y * g x - 2) (S R k) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k + 1)) ^ 2 -
        (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R k) * Polynomial.eval (f y * g x - 2) (S R (k + 1)) =
      1
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)) *
            (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) +
              Polynomial.eval (f y * g x - 2) (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval (f y * g x - 2) (S R ((↑m - 1) / 2)) *
          (Polynomial.eval (f y * g x - 2) (S R k) + Polynomial.eval (f y * g x - 2) (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
⊢ -(g z * 1) +
            Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k)) *
                (Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) +
                  Polynomial.eval (f y * g x - 2) (S R ((1 - 3) / 2 + k))) *
              ((g x * f z - g z) * (1 - 2 * 1) - f z * -(g x * 1)) +
          Polynomial.eval (f y * g x - 2) (S R ((1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R (1 / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 - 2) / 2 + k))) *
            ((f y * g z - f z) * -(g x * 1) - g z * (1 - 2 * 1)) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) *
            ((f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 1)) -
              Polynomial.eval (f y * g x - 2) (S R (1 + k))) +
          g z * 1) -
      (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 3) / 2 + k))) *
            ((g x * f z - g z) * 1) +
          Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 1) / 2 + k)) *
              (Polynomial.eval (f y * g x - 2) (S R ((1 + 1) / 2 + k)) +
                Polynomial.eval (f y * g x - 2) (S R ((1 + 1 - 2) / 2 + k))) *
            -(g z * 1) +
        (g z * Polynomial.eval (f y * g x - 2) (S R (1 - 1 + k)) * Polynomial.eval (f y * g x - 2) (S R (1 + k - 2)) +
          g z *
            (Polynomial.eval (f y * g x - 2) (S R (k - 1)) ^ 2 + Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1)) ^ 2 -
              (f y * g x - 2) * Polynomial.eval (f y * g x - 2) (S R (k - 1)) *
                Polynomial.eval (f y * g x - 2) (S R (k - 1 + 1))))) =
    0

Tactic:
ring_nf

Goal state after:
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)
⊢ ↑(2 * 1 * (2 ^ n * 2 ^ 1)) = ↑(2 ^ n * 2 ^ 2)

Tactic:
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 : U R (↑n + 1 + 1) = X * U R (↑n + 1) + T R (↑n + 1 + 1)
ih2 : U R (↑n + 1) = X * U R ↑n + T R (↑n + 1)
h₁ : U R (↑n + 1 + 2) = 2 * X * U R (↑n + 1 + 1) - U R (↑n + 1)
h₂ : U R (↑n + 2) = 2 * X * U R (↑n + 1) - U R ↑n
h₃ : T R (↑n + 1 + 2) = 2 * X * T R (↑n + 1 + 1) - T R (↑n + 1)
⊢ U R (↑n + 2 + 1) +
        (T R (↑n + 1 + 2) + X * U R (↑n + 2) + (2 * X * U R (↑n + 1 + 1) - U R (↑n + 1)) +
            2 * X * (X * U R (↑n + 1) + T R (↑n + 1 + 1)) +
          U R (↑n + 1)) -
      (X * U R (↑n + 2) + T R (↑n + 2 + 1) +
        (2 * X * T R (↑n + 1 + 1) - T R (↑n + 1) + X * (2 * X * U R (↑n + 1) - U R ↑n) + U R (↑n + 1 + 2) +
            2 * X * U R (↑n + 1 + 1) +
          (X * U R ↑n + T R (↑n + 1)))) =
    0

Tactic:
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 : U R (-↑n + 1) = X * U R (-↑n) + T R (-↑n + 1)
ih2 : U R (-↑n + 1 + 1) = X * U R (-↑n + 1) + T R (-↑n + 1 + 1)
h₁ : U R (-↑n - 1 + 2) = 2 * X * U R (-↑n - 1 + 1) - U R (-↑n - 1)
h₂ : U R (-↑n + 2) = 2 * X * U R (-↑n + 1) - U R (-↑n)
h₃ : T R (-↑n + 2) = 2 * X * T R (-↑n + 1) - T R (-↑n)
⊢ U R (-↑n - 1 + 1) +
        (T R (-↑n + 2) + (2 * X * U R (-↑n + 1) - U R (-↑n)) + X * U R (-↑n - 1 + 2) + U R (-↑n + 1 + 1) +
          2 * X * (X * U R (-↑n) + T R (-↑n + 1))) -
      (X * U R (-↑n - 1) + T R (-↑n - 1 + 1) +
        (2 * X * T R (-↑n + 1) - T R (-↑n) + U R (-↑n + 2) + X * (2 * X * U R (-↑n - 1 + 1) - U R (-↑n - 1)) +
            (X * U R (-↑n + 1) + T R (-↑n + 1 + 1)) +
          2 * X * U R (-↑n + 1))) =
    0

Tactic:
ring_nf

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

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

Tactic:
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₁ : U R (n + 1) = X * U R n + T R (n + 1)
h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)
h₃ : U R (n + 2) = 2 * X * U R (n + 1) - U R n
⊢ T R (n + 2) + (2 * X * U R (n + 1) - U R n + U R (n + 1 + 1) + X * (X * U R n + T R (n + 1))) -
      (X * T R (n + 1) - (1 - X ^ 2) * U R n + (U R (n + 2) + (X * U R (n + 1) + T R (n + 1 + 1)) + X * U R (n + 1))) =
    0

Tactic:
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 + 2) = -U R n - X * -U R (n + 1)
⊢ T R (n + 2) + (-U R n - X * -U R (n + 1)) - (X * U R (n + 1) - U R n + T R (n + 2)) = 0

Tactic:
ring_nf

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

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

Tactic:
linear_combination (norm := ring_nf) h

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
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 : C R (-(↑n + 1)) = C R (↑n + 1)
ih2 : C R (-↑n) = C R ↑n
h₁ : C R (↑n + 2) = X * C R (↑n + 1) - C R ↑n
h₂ : C R (-↑n - 2) = X * C R (-↑n - 1) - C R (-↑n)
⊢ C R (-(↑n + 2)) + (X * C R (↑n + 1) + C R (-↑n) + C R (↑n + 2) + (X * C R (-↑n - 1) - C R (-↑n))) -
      (C R (↑n + 2) + (X * C R (-(↑n + 1)) + C R ↑n + (X * C R (↑n + 1) - C R ↑n) + C R (-↑n - 2))) =
    0

Tactic:
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 : C R (- -↑n) = C R (-↑n)
ih2 : C R (-(-↑n + 1)) = C R (-↑n + 1)
h₁ : C R (↑n + 1) = X * C R ↑n - C R (↑n - 1)
h₂ : C R (-↑n - 1) = X * C R (-↑n) - C R (-↑n + 1)
⊢ C R (-(-↑n - 1)) + (X * C R (-↑n) + C R (-(-↑n + 1)) + (X * C R ↑n - C R (↑n - 1)) + C R (-↑n - 1)) -
      (C R (-↑n - 1) + (X * C R (- -↑n) + C R (-↑n + 1) + C R (↑n + 1) + (X * C R (-↑n) - C R (-↑n + 1)))) =
    0

Tactic:
ring_nf

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

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
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 : S R (-(↑n + 1) - 1) = -S R (↑n + 1 - 1)
ih2 : S R (-↑n - 1) = -S R (↑n - 1)
h₁ : S R (↑n + 1) = X * S R ↑n - S R (↑n - 1)
h₂ : S R (-↑n - 1 - 2) = X * S R (-↑n - 1 - 1) - S R (-↑n - 1)
⊢ S R (-(↑n + 2) - 1) +
        (X * -S R (↑n + 1 - 1) + S R (-↑n - 1) + (X * S R ↑n - S R (↑n - 1)) +
          (X * S R (-↑n - 1 - 1) - S R (-↑n - 1))) -
      (-S R (↑n + 2 - 1) + (X * S R (-(↑n + 1) - 1) + -S R (↑n - 1) + S R (↑n + 1) + S R (-↑n - 1 - 2))) =
    0

Tactic:
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 : S R (- -↑n - 1) = -S R (-↑n - 1)
ih2 : S R (-(-↑n + 1) - 1) = -S R (-↑n + 1 - 1)
h₁ : S R ↑n = X * S R (↑n - 1) - S R (↑n - 2)
h₂ : S R (-↑n - 2) = X * S R (-↑n - 1) - S R (-↑n)
⊢ S R (-(-↑n - 1) - 1) +
        (X * -S R (-↑n - 1) + S R (-(-↑n + 1) - 1) + (X * S R (↑n - 1) - S R (↑n - 2)) +
          (X * S R (-↑n - 1) - S R (-↑n))) -
      (-S R (-↑n - 1 - 1) + (X * S R (- -↑n - 1) + -S R (-↑n + 1 - 1) + S R ↑n + S R (-↑n - 2))) =
    0

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
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 : 2 * S R (↑n + 1 + 1) = X * S R (↑n + 1) + C R (↑n + 1 + 1)
ih2 : 2 * S R (↑n + 1) = X * S R ↑n + C R (↑n + 1)
h₁ : S R (↑n + 1 + 2) = X * S R (↑n + 1 + 1) - S R (↑n + 1)
h₂ : S R (↑n + 2) = X * S R (↑n + 1) - S R ↑n
h₃ : C R (↑n + 1 + 2) = X * C R (↑n + 1 + 1) - C R (↑n + 1)
⊢ 2 * S R (↑n + 2 + 1) +
        (C R (↑n + 1 + 2) + X * S R (↑n + 2) + 2 * (X * S R (↑n + 1 + 1) - S R (↑n + 1)) +
            X * (X * S R (↑n + 1) + C R (↑n + 1 + 1)) +
          2 * S R (↑n + 1)) -
      (X * S R (↑n + 2) + C R (↑n + 2 + 1) +
        (X * C R (↑n + 1 + 1) - C R (↑n + 1) + X * (X * S R (↑n + 1) - S R ↑n) + 2 * S R (↑n + 1 + 2) +
            X * (2 * S R (↑n + 1 + 1)) +
          (X * S R ↑n + C R (↑n + 1)))) =
    0

Tactic:
ring_nf

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case neg
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
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
aux : ∀ (a b : ℤ), autoParam (a + b = -3) reflection_mul_reflection_zpow_apply._auto_1_2 → a / 2 = -(b / 2) - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 2) / 2)) *
          (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
        ((f y * g z - f z) • x - g z • y) =
    z +
        (-Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (-Polynomial.eval t (S R ((↑m - 2) / 2)) + -Polynomial.eval t (S R (↑m / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (-Polynomial.eval t (S R ((↑m - 2) / 2)) *
          (-Polynomial.eval t (S R ((↑m - 3) / 2)) + -Polynomial.eval t (S R ((↑m - 1) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
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 : 2 * S R (-↑n + 1) = X * S R (-↑n) + C R (-↑n + 1)
ih2 : 2 * S R (-↑n + 1 + 1) = X * S R (-↑n + 1) + C R (-↑n + 1 + 1)
h₁ : S R (-↑n - 1 + 2) = X * S R (-↑n - 1 + 1) - S R (-↑n - 1)
h₂ : S R (-↑n + 2) = X * S R (-↑n + 1) - S R (-↑n)
h₃ : C R (-↑n + 2) = X * C R (-↑n + 1) - C R (-↑n)
⊢ 2 * S R (-↑n - 1 + 1) +
        (C R (-↑n + 2) + 2 * (X * S R (-↑n + 1) - S R (-↑n)) + X * S R (-↑n - 1 + 2) + 2 * S R (-↑n + 1 + 1) +
          X * (X * S R (-↑n) + C R (-↑n + 1))) -
      (X * S R (-↑n - 1) + C R (-↑n - 1 + 1) +
        (X * C R (-↑n + 1) - C R (-↑n) + 2 * S R (-↑n + 2) + X * (X * S R (-↑n - 1 + 1) - S R (-↑n - 1)) +
            (X * S R (-↑n + 1) + C R (-↑n + 1 + 1)) +
          X * (2 * S R (-↑n + 1)))) =
    0

Tactic:
ring_nf

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

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [S_two, C_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := S_add_two R (n + 1)
    have h₂ := S_add_two R n
    have h₃ := C_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_add_two R (-n - 1)
    have h₂ := S_add_two R (-n)
    have h₃ := C_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (X : R[X]) * ih1

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

Tactic:
by
  induction m using Int.negInduction with
  | nat m => exact_mod_cast reflection_mul_reflection_pow_apply hf hg m z t ht
  | neg _ m =>
    have ht' : t = g x * f y - 2 := by rwa [mul_comm (g x)]
    rw [zpow_neg, ← inv_zpow, mul_inv_rev, reflection_inv, reflection_inv, zpow_natCast,
      reflection_mul_reflection_pow_apply hg hf m z t ht', add_right_comm z]
    have aux (a b : ℤ) (hab : a + b = -3 := by lia) : a / 2 = -(b / 2) - 2 := by lia
    rw [aux (-m - 3) m, aux (-m - 2) (m - 1), aux (-m - 1) (m - 2), aux (-m) (m - 3)]
    simp only [S_neg_sub_two, Polynomial.eval_neg]
    ring_nf

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

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

Tactic:
ring_nf

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

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-↑n)) = T R' (-↑n)
ih2 : map f (T R (-↑n + 1)) = T R' (-↑n + 1)
⊢ map f (T R (-↑n - 1)) = T R' (-↑n - 1)

Tactic:
simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case a
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)
m : ℕ
ih :
  ((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
⊢ (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) * (1 - 2 * 1 - g x * -(f y * 1)) +
          Polynomial.eval t (S R (↑m - 1)) * -g x * (-(f y * 1) - 2 * -(f y * 1)) +
        Polynomial.eval t (S R (↑m + 1 - 2)) -
      ((Polynomial.eval t (S R (1 + ↑m)) + Polynomial.eval t (S R (1 + ↑m - 1))) * 1 +
        ((f y * g x - 2) * Polynomial.eval t (S R (↑m + 1 - 1)) - Polynomial.eval t (S R (↑m + 1)))) =
    0

Tactic:
ring_nf

Goal state after:
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
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)
m : ℕ
ih :
  ((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
⊢ (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) * -(g x * 1) +
      Polynomial.eval t (S R (↑m - 1)) * -g x * (1 - 2 * 1) =
    Polynomial.eval t (S R (1 + ↑m - 1)) * -g x * 1

Tactic:
ring_nf

Goal state after: