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 ^ (2 - 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:
push_cast

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.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:
push_cast

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 ^ (2 - 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:
push_cast

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.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 ^ (2 - 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:
push_cast

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.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:
push_cast

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.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:
push_cast

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

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.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:
push_cast

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

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

Goal state after:
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
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
h✝ : IsInteger A x
v : A
h : (algebraMap A K) v = x
⊢ (algebraMap A K) (num A x) = (algebraMap A K) (↑(den A x) * v)

Tactic:
simp only [map_mul, h]

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
h✝ : IsInteger A x
v : A
h : (algebraMap A K) v = x
⊢ (algebraMap A K) (num A x) = (algebraMap A K) ↑(den A x) * x
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
h₁ : C R (m + (-↑k - 1) + 2) = X * C R (m + (-↑k - 1) + 1) - C R (m + (-↑k - 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))

Tactic:
have h₂ := C_sub_two R (m - (-k - 1))

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
h₁ : C R (m + (-↑k - 1) + 2) = X * C R (m + (-↑k - 1) + 1) - C R (m + (-↑k - 1))
h₂ : C R (m - (-↑k - 1) - 2) = X * C R (m - (-↑k - 1) - 1) - C R (m - (-↑k - 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
o1 : O
ho1 : (algebraMap O R) o1 = 1
⊢ o0 ≠ o1

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
ho1 : (algebraMap O R) o0 = 1
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a b : ValueGroup A K), a * b = b * a

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
b✝ : ValueGroup A K
b : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b =
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
⊢ f = g

Tactic:
ext m

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ f m = g m
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
⊢ f = g

Tactic:
ext m

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
m : M
⊢ f m = g m
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
⊢ f = g

Tactic:
ext m

Goal state after:
R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
m : R
⊢ f m = g m
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : IsPrime (R ∙ q)
⊢ q ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
hQ1 : R ∙ 0 ≠ ⊥
hQ2 : IsPrime (R ∙ 0)
⊢ False
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : AdicCauchySequence I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n),
    (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m

Tactic:
by
    intro m n hmn
    simp only [mkQ_apply]
    exact (f.property hmn).symm

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
u : Rˣ
m : ℕ
h : p ∣ Classical.choose hR ^ m.succ * b
ha : ¬Classical.choose hR ^ m.succ * ↑u = 0
hm : ¬m.succ = 0
⊢ p ∣ Classical.choose hR ^ m.succ

Tactic:
rw [pow_succ']

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
u : Rˣ
m : ℕ
h : p ∣ Classical.choose hR ^ m.succ * b
ha : ¬Classical.choose hR ^ m.succ * ↑u = 0
hm : ¬m.succ = 0
⊢ p ∣ Classical.choose hR * Classical.choose hR ^ m
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)
c : 𝒪
hc : a = b * c
⊢ a * c = b ∨ b * c = a

Tactic:
exact Or.inr hc.symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ J.jacobson = J

Tactic:
← hj.2,

Goal state after:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ (map C j).jacobson = map C j
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose ⋯)
⊢ a = 0 → (addVal R) a = ⊤

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose ⋯)
⊢ (addVal R) 0 = ⊤
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case coe
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ OrderDual.toDual ((addVal R) (generator (ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ↑k))) = OrderDual.toDual ↑k

Tactic:
rw [OrderDual.toDual_inj, ENat.recTopCoe_natCast, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]

Goal state after:
case coe
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ Associated (generator (span {ϖ ^ k})) (ϖ ^ k)
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
hb₁ : 0 ∈ maximalIdeal R ^ n
hb₂ : 0 ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = 0 * m
⊢ False