mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).2
    else p) =
    p

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).2
    else p) =
    p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
cases lt_or_ge (degree p) (degree q)

Goal state after:
case pos.inl
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree < q.degree
⊢ (p %ₘ q).degree ≤ p.degree

case pos.inr
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : q.degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
unfold modByMonic divByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
eq : (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y
⊢ x = y

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
eq : (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y
⊢ x = y
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f

pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, (∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p

Tactic:
;

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, (∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p

Tactic:
;

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
unfold modByMonic divByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : 0 ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hp : 0 ≠ 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).1
    else 0) =
    0

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2)
        else (0, p)).1
    else 0) =
    0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p) (contract p f) = f

Tactic:
;

Goal state after:
case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p) (contract p f) = f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) ((expand R p) (map (iterateFrobenius R p k) ((expand R (p ^ k)) f))) =
    map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k)) f)

Tactic:
iterateFrobenius_add,

Goal state after:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) ((expand R p) (map (iterateFrobenius R p k) ((expand R (p ^ k)) f))) =
    map ((iterateFrobenius R p 1).comp (iterateFrobenius R p k)) ((expand R (p * p ^ k)) f)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0

Tactic:
;

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
| p %ₘ 1 + 1 * (p /ₘ 1)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
| p %ₘ 1 + 1 * (p /ₘ 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
;

Goal state after:
case inr.refine_1.e_a
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
a✝ : ℕ
⊢ a✝ ∈ Ioc n.succ p.natDegree ↔ a✝ ∈ Icc (n + 1 + 1) p.natDegree

Tactic:
;

Goal state after:
case inr.refine_1.e_a.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
a✝ : ℕ
⊢ a✝ ∈ Ioc n.succ p.natDegree ↔ a✝ ∈ Icc (n + 1 + 1) p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i

Tactic:
;

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.natDegree < (X - C a).natDegree

Tactic:
;

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.natDegree < (X - C a).natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ 0 < 1

Tactic:
;

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ i ∉ range (p.natDegree + 1) → (⇑derivative)^[i] p = 0

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ i ∉ range (p.natDegree + 1) → (⇑derivative)^[i] p = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p x✝¹ x✝ : R[X]
a✝ n✝ : ℕ
⊢ ((Finsupp.onFinset (range ((x✝¹ + x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ + x✝)) ⋯) a✝).coeff n✝ =
    ((Finsupp.onFinset (range (x✝¹.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝¹) ⋯ +
            Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯)
          a✝).coeff
      n✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p x✝¹ x✝ : R[X]
a✝ n✝ : ℕ
⊢ ((Finsupp.onFinset (range ((x✝¹ + x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ + x✝)) ⋯) a✝).coeff n✝ =
    ((Finsupp.onFinset (range (x✝¹.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝¹) ⋯ +
            Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯)
          a✝).coeff
      n✝
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x✝¹ : R
x✝ : R[X]
a✝ n✝ : ℕ
⊢ ((Finsupp.onFinset (range ((x✝¹ • x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ • x✝)) ⋯) a✝).coeff n✝ =
    (((RingHom.id R) x✝¹ • Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯) a✝).coeff n✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x✝¹ : R
x✝ : R[X]
a✝ n✝ : ℕ
⊢ ((Finsupp.onFinset (range ((x✝¹ • x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ • x✝)) ⋯) a✝).coeff n✝ =
    (((RingHom.id R) x✝¹ • Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯) a✝).coeff n✝
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter

Tactic:
;

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h
α : Type u_1
s : ℕ → Set α
⊢ (Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 ((fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) i)

Tactic:
;

Goal state after:
case h
α : Type u_1
s : ℕ → Set α
⊢ (Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 ((fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
f g : Filter α
s : Set α
a : α
⊢ ∀ (b : Set α) (x : α), (∀ (s : Set α), (∀ x ∈ b, x ∈ s) → x ∈ s) → x ∈ b

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
f g : Filter α
s : Set α
a : α
⊢ ∀ (b : Set α) (x : α), (∀ (s : Set α), (∀ x ∈ b, x ∈ s) → x ∈ s) → x ∈ b
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x ↦ m x i) l (f i)

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x ↦ m x i) l (f i)