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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
⊢ 1 ∈ S ^ card G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ S ^ card G * S ^ card G = S ^ card G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Semiring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha : IsOfFinOrder a
⊢ a = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : a ≤ 0
ha : IsOfFinOrder a
⊢ ¬a = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ |x| ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ c ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 ≤ p.divX.degree

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ (-1) ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
⊢ orderOf x ≤ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ X.degree ≤ (p.divX * X).degree

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ p.divX.degree < p.degree

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ ↑(card R) = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
⊢ ↑p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
this : n ∣ a.factorization p
⊢ a.factorization p = (n • factors) p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
h : p.divX = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i ≤ n, c = p ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X + C (p.coeff 0))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ ↑p ^ i = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
⊢ CharP R (p ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
⊢ m'.Coprime n'

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
⊢ g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ M p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ ¬0 < ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < degree 0
⊢ P 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (p + C a).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
h : p.coeff 0 = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (p * X).degree
h0 : ¬0 < p.degree
⊢ P (p * X)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : a = 0
⊢ (C a * X ^ (n + 1)).natDegree = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ M f

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
⊢ (f + g).coeff n = a + b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
⊢ (f * g).coeff d = if d = df + dg then a * b else 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.natDegree = deg

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
⊢ (f - g).coeff n = a - b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : ℤ
⊢ (↑a).coeff n = ↑(if n = 0 then a else 0)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ (expand R p) f = f.sum fun e a ↦ C a * (X ^ p) ^ e

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ (expand R p) ((monomial q) r) = (monomial (q * p)) r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
r : R
⊢ (expand R p) ((expand R q) (C r)) = (expand R (p * q)) (C r)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f✝ f g : R[X]
ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f
ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g
⊢ (expand R p) ((expand R q) (f + g)) = (expand R (p * q)) (f + g)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ (expand R p) ((expand R q) (C r * X ^ (n + 1))) = (expand R (p * q)) (C r * X ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
⊢ (expand R 0) f = C (eval 1 f)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
r : R
⊢ (expand R 1) (C r) = C r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) (f + g) = f + g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ (expand R (p ^ Nat.zero)) f = (⇑(expand R p))^[Nat.zero] f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f
⊢ (expand R (p ^ n.succ)) f = (⇑(expand R p))^[n.succ] f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ derivative ((expand R p) f) = (expand R p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ f.coeff 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ f.coeff d = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (n * p) = f.coeff n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (p * n) = f.coeff n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ g.coeff k = g'.coeff k

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ (expand R p) f = C r ↔ f = C r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : R[X]
x : S
hx : (aeval x) q = 0
⊢ (aeval x) (p %ₘ q) = (aeval x) p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
⊢ X ^ n ∣ f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ p.leadingCoeff ^ (q.natDegree + 1) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ ↑0 < ↑p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

Tactic:
by

Goal state after:
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 q : R[X]
⊢ ((p + q).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) =
    (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
x : S
hx : x ∈ (algebraMap R S).range
⊢ (aeval x) p ≠ 0

Tactic:
by

Goal state after:
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]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = (RingHom.id R) a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
⊢ 0 < 1 * p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).leadingCoeff = f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).Monic ↔ f.Monic

Tactic:
by

Goal state after: