mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (_root_.iterateFrobenius S p n) (f • s) =
    (_root_.iterateFrobenius R p n) f • (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (_root_.iterateFrobenius S p n) (f • s) =
    (_root_.iterateFrobenius R p n) f • (↑↑(_root_.iterateFrobenius S p n)).toFun s
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
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 b a✝ : G
⊢ (x /ᵒᶠ (a + b)).coeff a✝ = (x /ᵒᶠ a /ᵒᶠ b).coeff a✝

Tactic:
simp [add_assoc]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ n

Tactic:
by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n

Tactic:
nth_rw 2 [← prod_factorization_pow_eq_self hn]
  rw [eq_comm]
  apply Finset.prod_subset_one_on_sdiff
  · exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩
  · intro p hp
    obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
    rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
    simp [Finsupp.notMem_support_iff.mp hp2]
  · intro p hp
    simp [factorization_def n (prime_of_mem_primeFactors hp)]

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
⊢ card ↑(S ^ card G) = card ↑(S ^ card G * S ^ card G)

Tactic:
[

Goal state after:
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
⊢ card ↑(S ^ card G) = card ↑(S ^ card G * S ^ card G)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inl.inl
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)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0

Tactic:
eq_C_of_natDegree_eq_zero hp,

Goal state after:
case refine_2.inl.inl
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)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (C (p.coeff 0) + q).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inl.inr
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)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_

Goal state after:
case refine_2.inl.inr
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)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ M (p + q)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inr.inl
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)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
refine Or.inr ?_

Goal state after:
case refine_2.inr.inl
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)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (p + q)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
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 ∨ M (C a * X ^ (n + 1))

Tactic:
refine Or.inr ?_

Goal state after:
case neg
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
⊢ M (C a * X ^ (n + 1))
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:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ (expand R p) ((monomial q) r) = (monomial (q * p)) r
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:
[

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

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

Goal state after:
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))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a ↦ C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a ↦ C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
[

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : ¬q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)
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:
[

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))
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
  classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert! (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]

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

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).leadingCoeff = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
have := rootMultiplicity_mul_X_sub_C_pow (a := a) (n := n) C.map_one_ne_zero
  rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
intro hp

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (p %ₘ q).degree < q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
by
  convert! derivative_C_mul_X_pow (1 : R) n <;> 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) * ((expand R p) g).coeff (x.2 * p) =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p) * ((expand R p) g).coeff (x.2 * p) =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
eq_C_of_natDegree_eq_zero hp,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative (C (p.coeff 0)) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

Tactic:
[

Goal state after:
R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)
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 : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

Tactic:
[

Goal state after:
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)
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 = (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 = (x.1 + x.2) * p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
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:
[

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ (x * p, y * p) = (p * x, p * y)

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ (x * p, y * p) = (p * x, p * 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
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (f.coeff 0)

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Goal state after:
case inl
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)
⊢ IsUnit (f.coeff 0)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p a * f + contract p b * g = 1

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p a * f + contract p b * g = 1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime ((C a * X + C b).coeff 0) ((C a * X + C b).coeff 1)

Tactic:
simpa using hab.symm

Goal state after:
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 (iterateFrobenius R p k) ((expand R (p ^ k)) f) ^ p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f)

Tactic:
[

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 (iterateFrobenius R p k) ((expand R (p ^ k)) f) ^ p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (derivative p) = p.sum fun n a ↦ a * ↑n * x ^ (n - 1)

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (derivative p) = p.sum fun n a ↦ a * ↑n * x ^ (n - 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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)) g * (X - C r) ^ (p ^ n * rootMultiplicity (r ^ p ^ n) f))

Tactic:
rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0),

Goal state after:
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)) g) + p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ x ∈ range (n + 1),
      ↑(n.choose x) *
        (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q +
          (⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q)) =
    ∑ x ∈ range (n + 1), ↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
      ∑ x ∈ range (n + 1), ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ x ∈ range (n + 1),
      ↑(n.choose x) *
        (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q +
          (⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q)) =
    ∑ x ∈ range (n + 1), ↑(n.choose x) * (derivative ((⇑derivative)^[n - x] p) * (⇑derivative)^[x] q) +
      ∑ x ∈ range (n + 1), ↑(n.choose x) * ((⇑derivative)^[n - x] p * derivative ((⇑derivative)^[x] q))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
[

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
[

Goal state after:
case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.degree
⊢ False

Tactic:
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
eq_C_of_natDegree_eq_zero hp,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree = 0
⊢ derivative (C (p.coeff 0)) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
by
  classical
  have : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
[

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)

Tactic:
this

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)