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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ multiplicity (X - C x) p + multiplicity (X - C x) q = multiplicity (X - C x) p + multiplicity (X - C x) q

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
]

Goal state after:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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 /ₘ q = 0
this : p.degree < q.degree
⊢ p.degree < q.degree

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p.degree < q.degree
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Tactic:
]

Goal state after:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ f = f

Tactic:
]

Goal state after:
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
⊢ (0, p).1 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree ≤ p.degree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ ¬p /ₘ q = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ ¬p /ₘ q = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ a ^ p + b ^ p = a ^ p + b ^ p

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ 1 + ↑t.card ≤ 1 + (p /ₘ (X - C x)).degree

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ 1 + ↑t.card ≤ 1 + (p /ₘ (X - C x)).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p

Tactic:
]

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ 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
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ degree 0 < ↑p.natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ degree 0 < ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
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
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1))

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
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p.degree ≠ ⊥

Tactic:
degree_ne_bot

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ 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
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

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
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

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.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree

Tactic:
]

Goal state after:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree

Tactic:
]

Goal state after:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
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
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

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
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

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.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ 1 + count x t = 1 + count x t

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
]

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = (f /ₘ g).natDegree

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a t = count a t

Tactic:
]

Goal state after:
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
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))

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
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ p ^ 1 * rootMultiplicity (r ^ p ^ 1) f = p ^ 1 * rootMultiplicity (r ^ p ^ 1) f

Tactic:
]

Goal state after:
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 : ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
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 ((expand R p) f)
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 ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ¬∃ x, p.IsRoot x
a : R
⊢ 0 = 0

Tactic:
]

Goal state after:
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.natDegree ≤ ↑g.natDegree + ↑(q - f /ₘ g).natDegree

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.natDegree ≤ ↑g.natDegree + ↑(q - f /ₘ g).natDegree
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.coeff 0)

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.coeff 0)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible f
⊢ Irreducible f

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible f
⊢ Irreducible f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R (p * p ^ n)) f)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R (p * p ^ n)) 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.degree + (q - f /ₘ g).degree = g.degree + (q - f /ₘ g).degree

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
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
]

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ (aeval x) x_1 = 0)) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 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
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), IsAlgebraic R x

Tactic:
]

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), IsAlgebraic R x
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
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval ↑x) p = 0

Tactic:
]

Goal state after: