mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k

Tactic:
· rintro ⟨j, hjk, rfl⟩
    exact ⟨⟨j, le_of_lt hjk, rfl⟩, Nat.pow_lt_pow_of_lt pp.one_lt hjk⟩

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
· have : NeZero b := ⟨hb⟩
    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n).natAbs * m.natAbs

Tactic:
Int.natAbs_natCast

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ φ k = ψ k

Tactic:
rw [φ.ext_int ψ]

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

Goal state before:
pp: case zero
m : ℕ
hb : 1 < 0
⊢ m < 0 ^ (digits 0 m).length

Tactic:
simp_all [lt_base_pow_length_digits']

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

Goal state before:
pp: case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m < (0 + 1) ^ ((0 + 1).digits m).length

Tactic:
simp_all [lt_base_pow_length_digits']

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

Goal state before:
pp: case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Tactic:
simp_all [lt_base_pow_length_digits']

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []

Tactic:
change k ∣ 0 - 0

Goal state after:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≤ multiplicity a b
⊢ ↑n ≤ emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

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

Goal state before:
pp: b f n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
ih :
  True →
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
exact ih trivial

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p n : ℕ
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
rcases eq_or_ne p 1 with rfl | hp
  · simp
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [← padicValNat_eq_emultiplicity_of_ne_one, *]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity, ← padicValNat_def' ha.ne_one hb,
    Nat.cast_le]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
conv_rhs => rw [h]

Goal state after:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
conv_rhs => rw [h]

Goal state after:
case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 1 ↔ x = 1

Tactic:
by
  rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ x ^ orderOf x = 1

Tactic:
← map_pow,

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ (x ^ orderOf x) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

Tactic:
exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt

Goal state after:
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 = 1
⊢ False

Tactic:
exact hp this

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ n !.factorization p ≤ n / (p - 1)

Tactic:
rw [factorization_factorial hp (Nat.lt_add_one (log p n))]
  exact Nat.geom_sum_Ico_le hp.two_le _ _

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ n !.factorization p ≤ n / (p - 1)

Tactic:
by
  rw [factorization_factorial hp (Nat.lt_add_one (log p n))]
  exact Nat.geom_sum_Ico_le hp.two_le _ _

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

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
⊢ (n.choose k).factorization p = 0

Tactic:
rcases em' p.Prime with hp | hp
  · exact factorization_eq_zero_of_not_prime (choose n k) hp
  rcases lt_or_ge n k with hnk | hkn
  · simp [choose_eq_zero_of_lt hnk]
  simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff,
    mem_Ico, not_le, and_imp]
  intro i hi₁ hi
  rcases eq_or_lt_of_le hi₁ with (rfl | hi)
  · rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
    exact
      lt_of_le_of_lt
        (add_le_add
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk'))
            ((n - k) % p)))
        (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])
  · replace hn : n < p ^ i := by
      have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
      calc
        n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
    rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]
  exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

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 ^ (n - m + m) = a ^ n

Tactic:
by simp [tsub_add_cancel_of_le hmn.le]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤ →
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x =
      ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + emultiplicity p (n + 1) + 1

Tactic:
add_assoc

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤ →
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x =
      ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rcases eq_or_ne e 0 with (rfl | he_pos)

Goal state after:
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (n + 1) + (emultiplicity p n ! + ↑n) = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n

Tactic:
add_assoc

Goal state after:
case succ.e_a
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (n + 1) + (emultiplicity p n ! + ↑n) = emultiplicity p (n + 1) + (emultiplicity p n ! + ↑n)
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ (x + y) ^ p - y ^ p

Tactic:
add_pow_prime_eq hpri,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) - y ^ p
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
have hx_mem : x ∈ zpowers y := by simp [← h]

Goal state after:
G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
hx_mem : x ∈ zpowers y
⊢ x = y ∨ x⁻¹ = y
Module: Mathlib.Data.Nat.Factorization.Basic

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

pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
· symm at h
    by_cases hm0 : m = 0
    · simp_all
    · use 0
      simp_all

Goal state after:
case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
suffices ha : a = c ^ n by
    refine ⟨ha, ?_⟩
    apply Nat.pow_left_injective hn0
    simp [← h, ha, Nat.pow_right_comm]

Goal state after:
case h
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
⊢ a = c ^ n
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
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'

Tactic:
conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]

Goal state after:
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'
⊢ a ^ m' = b ^ n'
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:
rwa [eq_C_of_degree_le_zero h, ← C_add, heq0, zero_add] at h0

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.coeff (n / p) = 0

pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0

Tactic:
· rw [coeff_eq_zero_of_natDegree_lt]
      contrapose! hn
      norm_cast
      rw [← Nat.div_mul_cancel hpn]
      exact Nat.mul_le_mul_right p hn

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
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
⊢ False

Tactic:
add_assoc

Goal state after:
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)
⊢ False
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:
have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
  refine le_antisymm ?_ ?_
  · rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
    exact pow_rootMultiplicity_not_dvd h a
  · rw [le_rootMultiplicity_iff h2, pow_add]
    exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
by
  nontriviality R
  have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
  have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
    rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
  have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
    calc
      degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
      _ ≤ _ := by
        rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
        exact Nat.le_add_right _ _
  calc
    degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
    _ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
    _ = _ := congr_arg _ (modByMonic_add_div _ _)

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

Tactic:
add_assoc

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)) =
    ∑ 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))
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
rw [le_principal_iff]
    refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_
    exact mem_iInf_of_mem j (mem_principal_self _)

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

Goal state before:
pp: case zero
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
⊢ s ↑(x 0) ∈ f

Tactic:
apply hs.set_index_mem

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

Goal state before:
pp: case succ
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
n✝ : ℕ
⊢ s ↑(x (n✝ + 1)) ∈ f

Tactic:
apply hs.set_index_mem

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : Filter α
g : Filter β
⊢ (f ×ˢ g).ker = f.ker ×ˢ g.ker

Tactic:
simp [Set.prod_eq, Filter.prod_eq_inf]

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
have V_in : ∀ (i : I), V i ∈ s i := by
      rintro i
      have : ⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
      exact mem_of_superset this subset_union_right

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
hV₁ : ∀ (i : ↑I), ∃ t, (∀ (i_1 : p ↑i), s ↑i ⊆ t i_1) ∧ V i = ⋂ (i : p ↑i), t i
⊢ ∃ I_1, I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ ⋂ i ∈ I_1, s i ⊆ ⋂ i, V i

Tactic:
choose! t ht₁ ht₂ using hV₁

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ∃ I_1, I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ ⋂ i ∈ I_1, s i ⊆ ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
by
  rw [le_rootMultiplicity_iff hpq, pow_add]
  gcongr <;> apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (univ.pi s) = ⊥

Tactic:
simp only [inf_principal_eq_bot]
    rintro ⟨i, hi⟩
    filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f

Tactic:
rw [← Coheyting.inf_hnot_self, inf_eq_left, le_cofinite_iff_ker,
    Filter.hnot_def, le_principal_iff]

Goal state after:
α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s

Tactic:
apply le_smul_of_one_le_left (hw s)

Goal state after:
σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ 1 ≤ f s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ n • X.roots = replicate n 0

Tactic:
roots_X,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ n • {0} = replicate n 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (X ^ n - C a).degree ≤ ↑n

Tactic:
by
            rw [hn, pow_zero, ← C_1, ← map_sub]
            exact degree_C_le

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

Goal state before:
pp: case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f x ^ n = f a

Tactic:
← map_pow,

Goal state after:
case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f (x ^ n) = f a