mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ring_nf

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) +
          Polynomial.eval t (S R (-↑m - 1)) * -g x * -(f y * 1) +
        Polynomial.eval t (S R (-↑m - 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)) - Polynomial.eval t (S R (-↑m)))) =
    0

Tactic:
ring_nf

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))) * (-(g x * 1) - 2 * -(g x * 1)) +
          Polynomial.eval t (S R (-↑m - 1)) * -g x * (1 - 2 * 1 - f y * -(g x * 1)) +
        g x * ((f y * g x - 2) * Polynomial.eval t (S R (-↑m - 1)) - Polynomial.eval t (S R (-↑m))) -
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x * 1 + g x * Polynomial.eval t (S R (-↑m - 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 : 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:
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:
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 ^ 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:
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:
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 ^ 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:
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 ^ 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:
ring_nf

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

Goal state before:
pp: 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)) = 3 * X * derivative (U R n) - (↑n + 2) * ↑n * U R n

Tactic:
linear_combination (norm := (push_cast; 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 : ℤ
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:
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 + 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) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h

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.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
⊢ ∃ a, (p.compl₁₂ i j) a = f

Tactic:
set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N := f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF : F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
⊢ ∃ a, (p.compl₁₂ i j) a = f
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:
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.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 + 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) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h

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.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝⁴ : p.IsPerfPair
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
⊢ Bijective ⇑(p.compl₁₂ i j)

Tactic:
refine ⟨LinearMap.ker_eq_bot.mp <| eq_bot_iff.mpr fun m hm ↦ ?_, fun f ↦ ?_⟩
  · replace hm : i m ∈ j.range.dualAnnihilator.map (p.toPerfPair.symm : Dual R N →ₗ[R] M) := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator]
      refine ⟨p.toPerfPair (i m), ?_, LinearEquiv.symm_apply_apply _ _⟩
      rintro - ⟨n, rfl⟩
      simpa using LinearMap.congr_fun hm n
    suffices i m ∈ (⊥ : Submodule R M) by simpa [hi] using this
    simpa only [← hij.isCompl_left.inf_eq_bot, Submodule.mem_inf]
      using ⟨LinearMap.mem_range_self i m, hm⟩
  · set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF
    have hF (n : N') : F (j n) = f n := by simp [hF]
    set m : M := p.toPerfPair.symm F with hm
    obtain ⟨-, y, ⟨m₀, rfl⟩, hy, hm'⟩ :=
      Submodule.codisjoint_iff_exists_add_eq.mp hij.isCompl_left.codisjoint m
    refine ⟨m₀, LinearMap.ext fun n ↦ ?_⟩
    replace hy : (p y) (j n) = 0 := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy
      obtain ⟨g, hg, rfl⟩ := hy
      simpa using hg _ (LinearMap.mem_range_self j n)
    rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm] at hm'
    simpa [← hF, ← LinearMap.congr_fun hm' (j n)]

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] (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:
ring_nf

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

Goal state before:
pp: 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))

Tactic:
linear_combination (norm := (push_cast; 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 : ℤ
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:
ring_nf

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

Goal state before:
pp: 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))

Tactic:
linear_combination (norm := (push_cast; 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 : ℤ
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:
ring_nf

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

Goal state before:
pp: 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))

Tactic:
linear_combination (norm := (push_cast; 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 : ℤ
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:
ring_nf

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

Goal state before:
pp: 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))

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h

Goal state after:
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: case h
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ (algebraMap A K) (↑d⁻¹ * num A x) = x

Tactic:
refine _root_.trans ?_ (mk'_num_den A x)

Goal state after:
case h
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : (algebraMap A K) ↑(den A x) ≠ 0
⊢ (algebraMap A K) (↑d⁻¹ * num A x) = mk' K (num A x) (den A x)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x⁻¹⁻¹) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)

Tactic:
rw [inv_inv] at this

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
this : Associated (num A x) ↑(den A x⁻¹)
⊢ Associated (num A x) ↑(den A x⁻¹)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (↑k + 1) = T R (m + (↑k + 1)) + T R (m - (↑k + 1))
ih2 : 2 * T R m * T R ↑k = T R (m + ↑k) + T R (m - ↑k)
h₁ : T R (m + ↑k + 2) = 2 * X * T R (m + ↑k + 1) - T R (m + ↑k)
h₂ : T R (m - ↑k - 2) = 2 * X * T R (m - ↑k - 1) - T R (m - ↑k)
h₃ : T R (↑k + 2) = 2 * X * T R (↑k + 1) - T R ↑k
⊢ 2 * T R m * T R (↑k + 2) +
        (2 * T R m * (2 * X * T R (↑k + 1) - T R ↑k) + T R (m - ↑k - 2) + T R (m + ↑k + 2) + 2 * T R m * T R ↑k +
          2 * X * (T R (m + (↑k + 1)) + T R (m - (↑k + 1)))) -
      (T R (m + (↑k + 2)) + T R (m - (↑k + 2)) +
        (2 * T R m * T R (↑k + 2) + (2 * X * T R (m - ↑k - 1) - T R (m - ↑k)) +
              (2 * X * T R (m + ↑k + 1) - T R (m + ↑k)) +
            (T R (m + ↑k) + T R (m - ↑k)) +
          2 * X * (2 * T R m * T R (↑k + 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
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (-↑k) = T R (m + -↑k) + T R (m - -↑k)
ih2 : 2 * T R m * T R (-↑k + 1) = T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))
h₁ : T R (m + (-↑k - 1) + 2) = 2 * X * T R (m + (-↑k - 1) + 1) - T R (m + (-↑k - 1))
h₂ : T R (m - (-↑k - 1) - 2) = 2 * X * T R (m - (-↑k - 1) - 1) - T R (m - (-↑k - 1))
h₃ : T R (-↑k - 1 + 2) = 2 * X * T R (-↑k - 1 + 1) - T R (-↑k - 1)
⊢ 2 * T R m * T R (-↑k - 1) +
        (2 * T R m * (2 * X * T R (-↑k - 1 + 1) - T R (-↑k - 1)) + T R (m - (-↑k - 1) - 2) + T R (m + (-↑k - 1) + 2) +
            2 * T R m * T R (-↑k + 1) +
          2 * X * (T R (m + -↑k) + T R (m - -↑k))) -
      (T R (m + (-↑k - 1)) + T R (m - (-↑k - 1)) +
        (2 * T R m * T R (-↑k - 1 + 2) + (2 * X * T R (m - (-↑k - 1) - 1) - T R (m - (-↑k - 1))) +
              (2 * X * T R (m + (-↑k - 1) + 1) - T R (m + (-↑k - 1))) +
            (T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))) +
          2 * X * (2 * T R m * T R (-↑k)))) =
    0

Tactic:
ring_nf

Goal state after: