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

Goal state after:
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
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
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
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
x✝ : M
⊢ (LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) x✝ = 0 x✝

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
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
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
x✝ : M
⊢ (LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) x✝ = 0 x✝
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:
;

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

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

Goal state before:
pp: case refine_1
ι : 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
hx : x ∈ span R (range ⇑P.root)
⊢ (P.reflection i) x = (P.reflection j) x

Tactic:
induction hx using Submodule.span_induction with

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

Goal state after:
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
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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : x ∈ span R (⇑P.root '' s)
⊢ (P.reflection j) x = x

Tactic:
induction hx using Submodule.span_induction with

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

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)
⊢ (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
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 : M
f : Dual R M
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ 2 * 2 = 4

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ 2 * 2 = 4
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : (A' * B').map ⇑K.subtype = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1

Tactic:
simp_rw [Matrix.map_mul] at hB

Goal state after:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A'.map ⇑K.subtype * B'.map ⇑K.subtype = map 1 ⇑K.subtype
⊢ A * (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = 1
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:
;

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)
⊢ (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
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:
;

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) := ⋯
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := ⋯
hf : Injective ⇑f
hg : Injective ⇑g
x✝¹ : A
x✝ : ↥p
⊢ ↑(((AlgebraTensorModule.curry (↑R (tensorToSpan A p))) x✝¹) x✝) = ↑(((AlgebraTensorModule.curry (↑R f ∘ₗ g)) x✝¹) x✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) := ⋯
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := ⋯
hf : Injective ⇑f
hg : Injective ⇑g
x✝¹ : A
x✝ : ↥p
⊢ ↑(((AlgebraTensorModule.curry (↑R (tensorToSpan A p))) x✝¹) x✝) = ↑(((AlgebraTensorModule.curry (↑R f ∘ₗ g)) x✝¹) x✝)
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case add
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
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑j.range
hy✝ : y✝ ∈ span R ↑j.range
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p (i x)) x✝ + (p (i x)) y✝ = 0

Tactic:
;

Goal state after:
case add
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
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n x✝ y✝ : N
hx✝ : x✝ ∈ span R ↑j.range
hy✝ : y✝ ∈ span R ↑j.range
a✝¹ : (p (i x)) x✝ = 0
a✝ : (p (i x)) y✝ = 0
⊢ (p (i x)) x✝ + (p (i x)) y✝ = 0
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case smul
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
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R ↑j.range
a✝ : (p (i x)) x✝ = 0
⊢ a✝¹ • (p (i x)) x✝ = 0

Tactic:
;

Goal state after:
case smul
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
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
a✝¹ : R
x✝ : N
hx✝ : x✝ ∈ span R ↑j.range
a✝ : (p (i x)) x✝ = 0
⊢ a✝¹ • (p (i x)) x✝ = 0
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Subsingleton R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

pp: case inr
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Nontrivial R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

Tactic:
;

Goal state after:
case inl
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Subsingleton R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p

case inr
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Nontrivial A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra.IsEpi R A
inst✝⁶ : Flat R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Free R ↥p
inst✝ : Module.Finite R ↥p
h✝ : Nontrivial R
⊢ finrank A ↥(span A ↑p) = finrank R ↥p
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:
;

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

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