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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R

Tactic:
| inl hp =>

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

Goal state before:
pp: case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b

Tactic:
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha

Goal state after:
case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : I = ⊥
⊢ ker (mk I) = ⊥

Tactic:
rw [mk_ker, h]

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.mp
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
    · exact ⟨[], y :: ys, by simp⟩
    · exact ⟨y :: l₁, l₂, l0, by simp⟩

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x

Tactic:
by
  rcases le_total n m with h | h
  · refine left_of_add ?_ hn
    rwa [tsub_add_cancel_of_le h]
  · rw [tsub_eq_zero_iff_le.mpr h]
    apply isPeriodicPt_zero

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain (fun a b ↦ r (f^[a] x) (f^[b] x)) ↑(List.range (minimalPeriod f x)) ↔
    ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
← hM,

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain (fun a b ↦ r (f^[a] x) (f^[b] x)) ↑(List.range (minimalPeriod f x - succ 0 + succ 0)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d d' : α
x_mem : x ∈ [].dropLast
⊢ [].nextOr x d = [].nextOr x d'

Tactic:
cases x_mem

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit_chain r]

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ (∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : i = 1
⊢ l[i + (idxOf a l - 1)]? = some [l.prev a ha, a][i]

Tactic:
subst hi₁
    grind

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
have : (n + 1 + length tl) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
isPrimePow_nat_iff

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
isPrimePow_nat_iff

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
rw [isPrimePow_nat_iff_bounded_log]
  obtain rfl | h := eq_or_ne n 1
  · simp
  constructor
  · rintro ⟨k, hkle, hk_pos, p, hle, heq, hprime⟩
    refine ⟨k, hkle, hk_pos, ?_⟩
    rw [heq, hprime.pow_minFac hk_pos.ne']
  · rintro ⟨k, hkle, hk_pos, heq⟩
    refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
    · grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]
    · grind [Nat.minFac_prime_iff]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
n : ℕ
hn : (a :: l).rotate n = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
induction n generalizing a b l m with

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

Goal state before:
pp: case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Tactic:
use (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Goal state after:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Injective ⇑f
⊢ (H ⊔ f.ker).index * f.range.index = H.index * f.range.index

Tactic:
f.ker_eq_bot hf,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Injective ⇑f
⊢ (H ⊔ ⊥).index * f.range.index = H.index * f.range.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index ∣ 2 ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
by
  rw [index_dvd_two_iff, (Equiv.inv G).exists_congr]
  refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_
  simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton (MulAction.orbitRel.Quotient G X)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K

Tactic:
convert! pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K ↔ ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = n % ↑p + ↑p * (n / ↑p)

Tactic:
Int.emod_add_mul_ediv

Goal state after:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

Tactic:
rw [mem_divisors, zero_dvd_iff (a := n)] at h
    cases h.2 h.1

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ 0 ≤ (divisors 0).sup id

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
· apply zero_le

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i

Tactic:
pow_succ,

Goal state after:
case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / (b ^ i * b) * b ≤ a / b ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ (↑a.val).val < m + 1

Tactic:
val_cast_of_lt

Goal state after:
case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]

Tactic:
digits_add_two_add_one,

Goal state after:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
pow_succ,

Goal state after:
case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ m * a).val = a.val ^ (m + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ (m + 1)).val ≤ a.val ^ (m + 1)

Tactic:
pow_succ,

Goal state after:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ (m + 1)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat 0 n < n

Tactic:
simp [Nat.pos_of_ne_zero hn]

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat 1 n < n

Tactic:
simp [Nat.pos_of_ne_zero hn]

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

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
· rcases eq_or_ne n 0 with rfl | hn <;> simp [divMaxPow, *]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0

Tactic:
Nat.mul_one

Goal state after:
case e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length

Tactic:
simp only [Nat.toDigitsCore]; intro n l1 l2 hlen

Goal state after:
case zero
b n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ l1.length = l2.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length

Tactic:
simp only [Nat.toDigitsCore]; intro n l1 l2 hlen

Goal state after:
case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length ≤ l

Tactic:
rwa [digits_length_le_iff hb]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
emultiplicity_le_emultiplicity_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x ^ (2 * r + 1 + 1) = x

Tactic:
pow_succ,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x ^ (2 * r + 1) * x = x
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✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
← _root_.pow_succ,

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ (orderOf x - 1 + 1) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
apply add_left_injective d.factorization

Goal state after:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x ↦ x + d.factorization) (n / d).factorization =
    (fun x ↦ x + d.factorization) (n.factorization - d.factorization)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x))) = x ^ z

Tactic:
Int.emod_add_mul_ediv

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ z = x ^ z
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 hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0

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

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

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:
· rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div],
            (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ (n + 1) * k

Tactic:
pow_succ,

Goal state after:
case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ n * X * k
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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
| f ^ p ^ (k + 1)

Tactic:
pow_succ,

Goal state after:
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
| f ^ (p ^ k * p)
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:
by
  simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a 0 = 0

Tactic:
rootMultiplicity_zero

Goal state after:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ 0 = 0
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generate (sInter '' {t | t.Finite ∧ t ⊆ s}) = generate s

Tactic:
← generate_eq_generate_inter

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ generate s = generate s
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
by_cases hp : p.natDegree = 0
  · grind [natDegree_derivative_le]
  · simp [natDegree, degree_derivative hp]

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

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

Tactic:
pow_succ,

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

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

Tactic:
pow_succ,

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
classical
  rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

Goal state after:
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Tactic:
cases nonempty_fintype (PLift ι)
  rw [← iInf_plift_down, ← iInter_plift_down]
  simpa using iInf_principal_finset Finset.univ (f <| PLift.down ·)

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
rw [← principal_univ, mem_prod_principal]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
pow_succ,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * (X ^ n * X))) = eval₂ C q (derivative (C r * (X ^ n * X))) * derivative q
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ (∀ (x : α), {x}ᶜ ∈ f) ↔ ⋂ s ∈ f, s = ∅

Tactic:
iInter₂_eq_empty_iff

Goal state after:
α : Type u_2
f : Filter α
⊢ (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ i, ∃ (_ : i ∈ f), a ∉ i
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
| Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) p.roots

Tactic:
← p.map_roots_comp_C_mul_X_add_C a b ha

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
| Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) (Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
pow_succ,

Goal state after:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ n * p).roots = (n + 1) • p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod = (factors x).prod

Tactic:
by rw [toFinset_sum_count_nsmul_eq (factors x)]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
⊢ (nthRoots n a).card ≤ n

Tactic:
exact
  (if hn : n = 0 then
    if h : (X : R[X]) ^ n - C a = 0 then by
      simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]
    else
      WithBot.coe_le_coe.1
        (le_trans (card_roots h)
          (by
            rw [hn, pow_zero, ← C_1, ← map_sub]
            exact degree_C_le))
  else by
    rw [← Nat.cast_le (α := WithBot ℕ)]
    rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
    exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)

Tactic:
by
    rcases eq_or_ne a 0 with rfl | ha
    · simp
    · simp [mem_normalizedFactors_iff' ha,
        mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha), map_dvd_iff_dvd_symm,
        MulEquiv.irreducible_iff, he]

Goal state after: