mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ a.gcd b
⊢ False

Tactic:
Coprime.gcd_eq_one hab,

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ 1
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

Tactic:
simp

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

Goal state before:
pp: a b : ℕ
hb : b ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
  exact Dvd.intro b rfl

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

Goal state before:
pp: p n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ∣ n ↔ p ^ 1 ∣ n

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
hp : Prime p
⊢ (p * 0)!.factorization p = 0!.factorization p + 0

Tactic:
simp

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

Goal state before:
pp: case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ ¬False ∨ n / q ^ n.factorization q = 0

Tactic:
simp

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

Goal state before:
pp: m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / p ^ m.factorization p = m

Tactic:
exact (ordCompl_eq_self_iff_zero_or_not_dvd m hp).mpr (Or.inr hm)

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

Goal state before:
pp: p x : ℕ
x✝¹ : x + 1 ≤ 0
x✝ : x + 1 ≠ 0
⊢ (factorization 0) p ≤ (choose 0 (x + 1)).factorization p + (x + 1).factorization p

Tactic:
simp

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

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / p ^ n.factorization p

Tactic:
if hn0 : n = 0 then simp [hn0] else
  if hd0 : d = 0 then simp [hd0] at hpd else
  rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

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

Goal state before:
pp: case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d

Tactic:
simp

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

Goal state before:
pp: case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg.hg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

Tactic:
simp

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

Goal state before:
pp: case zero
p n : ℕ
h : 0 < p
⊢ 0!.factorization p = 0

Tactic:
simp

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

Goal state before:
pp: case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q

Tactic:
simp

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

Goal state before:
pp: case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

Tactic:
simp

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

Goal state before:
pp: case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ m = 1 * x ^ m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ↑(#({x ∈ Ico 1 b | p ^ x ∣ n + 1})))

Tactic:
simp

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

Goal state before:
pp: case pos
⊢ ∏ p ∈ primeFactors 0, p ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ m = 1 * a ^ m

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
simp

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
inst✝ : Group G
x y : G
i : ℤ
hx : IsOfFinOrder x
n : ℕ
⊢ (fun x_1 ↦ x ^ x_1) ↑n = x ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
p : ℕ
hp : Prime p
⊢ emultiplicity p (p * 0)! = emultiplicity p 0! + ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
⊢ orderOf 1 ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Tactic:
exact infinite_not_isOfFinOrder h <| Set.toFinite _

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
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
x✝ : ℕ
⊢ emultiplicity p x✝ ≤ emultiplicity p (x✝.choose 0) + emultiplicity p 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n✝ : ℕ
⊢ emultiplicity p 0 ≤ emultiplicity p (choose 0 (n✝ + 1)) + emultiplicity p (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = {i ∈ Ico 1 0 | p ^ i ∣ 0}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

Tactic:
simp [choose_eq_zero_of_lt hkp]

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

Goal state before:
pp: case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g a✝ : G
⊢ (0 /ᵒᶠ g).coeff a✝ = (coeff 0) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a✝ : G
⊢ (x /ᵒᶠ 0).coeff a✝ = x.coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x y : k[G]
g a✝ : G
⊢ ((x + y) /ᵒᶠ g).coeff a✝ = (x /ᵒᶠ g + y /ᵒᶠ g).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), (p + q).divX.coeff n = (p.divX + q.divX).coeff n

Tactic:
simp

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (C a * p).divX.coeff n✝ = (C a * p.divX).coeff n✝

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
⊢ (X ^ 0).divX = if 0 = 0 then 0 else X ^ (0 - 1)

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
⊢ #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p

Tactic:
simp

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:
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr.inl
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2

Tactic:
simp

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

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:
rcases p.eq_zero_or_pos with hp | hp

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

case inr
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ ((expand R p) f).natDegree = f.natDegree * p
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
  --`eval₂_modByMonic_eq_self_of_root` doesn't work here as it needs commutativity
  simp [modByMonic_eq_sub_mul_div, hx]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
hdeg : (p * 0).natDegree ≤ p.natDegree
⊢ p * 0 = p * C (p * 0).leadingCoeff

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (comp 0 (C a * X + C b)) ≤ rootMultiplicity (a * c + b) 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r a : R
⊢ eval r ((expand R p) (C a)) = eval (r ^ p) (C a)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ (aeval r) ((expand R p) (C a)) = (aeval (r ^ p)) (C a)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : (aeval r) ((expand R p) (C a * X ^ n)) = (aeval (r ^ p)) (C a * X ^ n)
⊢ (aeval r) ((expand R p) (C a * X ^ (n + 1))) = (aeval (r ^ p)) (C a * X ^ (n + 1))

Tactic:
simp

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

Goal state before:
pp: case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X = X - C 0

Tactic:
simp

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

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = C 1 * X ^ n

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 1 * ↑n

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (monomial (1 - 1)) (1 * ↑1) = 1

Tactic:
simp

Goal state after:
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 ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
· simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
⊢ (⇑derivative)^[0] (s • p) = s • (⇑derivative)^[0] p

Tactic:
simp

Goal state after:
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
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
hf

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
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (C (f.coeff 0))
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
simp

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

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

Tactic:
simp

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
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (iterateFrobenius R p 0) ((expand R (p ^ 0)) f) = f ^ p ^ 0

Tactic:
simp

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

Tactic:
simp

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

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

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

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (⇑derivative)^[0] (map f p) = map f ((⇑derivative)^[0] p)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
m : ℕ
⊢ ((⇑derivative)^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (⇑(aeval x) ∘ fun x ↦ X - C x) x = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
| (⇑derivative)^[k] p

Tactic:
(derivative^[k] p).as_sum_support_C_mul_X_pow

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
| ∑ i ∈ ((⇑derivative)^[k] p).support, C (((⇑derivative)^[k] p).coeff i) * X ^ i
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∀ (i : ℕ), (monomial i) 0 = 0

Tactic:
simp

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

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

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

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

Tactic:
apply coeff_eq_zero_of_natDegree_lt
    rw [natDegree_divByMonic p (monic_X_sub_C a), natDegree_X_sub_C]
    exact (Nat.pred_lt hp).trans_le h

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

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]
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:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ (C r).natDegree < (X - C a).natDegree

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) 0 = (Finsupp.single 0 (C r)) 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i✝ i : ℕ
⊢ (derivativeFinsupp (C r)) (i + 1) = (Finsupp.single 0 (C r)) (i + 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 0 = (Finsupp.single 0 X + Finsupp.single 1 1) 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 1 = (Finsupp.single 0 X + Finsupp.single 1 1) 1

Tactic:
simp

Goal state after: