mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ p ∣ y

Tactic:
assumption

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

Goal state before:
pp: case inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p

Tactic:
· refine (hy ?_).elim
    subst hap
    subst ha
    rw [sq, Nat.mul_eq_left (Nat.mul_ne_zero hp.ne_zero hp.ne_zero)] at h
    exact h

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f ∘ g)^[n] x

Tactic:
hco.comp_iterate

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f ∘ g)^[n] x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
hco.comp_iterate

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : x ∈ ys.dropLast → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' t)

Tactic:
convert! Equiv.refl ↑(t * s)

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' t = t * ↑s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, gp✝⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
assumption

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
a b : ↑(orbitRel.Quotient.orbit ω)
h : (orbitRel ↥H ↑(orbitRel.Quotient.orbit ω)) a b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
by
      simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h
      simp only [Quotient.eq] at h ⊢
      exact h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
⊢ ∀ (a b : X), (orbitRel (↥H) X) a b → ↑⋯.choose = ↑⋯.choose

Tactic:
intro y₁ y₂ h
    rw [orbitRel_apply] at h
    rw [Quotient.eq'', leftRel_eq]
    dsimp only
    rcases h with ⟨g, rfl⟩
    dsimp only
    suffices (exists_smul_eq G (g • y₂) x).choose = (exists_smul_eq G y₂ x).choose * g⁻¹ by
      simp [this]
    refine IsCancelSMul.right_cancel _ _ (g • y₂) ?_
    rw [(exists_smul_eq G (g • y₂) x).choose_spec, Subgroup.smul_def, Subgroup.coe_inv,
        smul_smul, inv_mul_cancel_right, (exists_smul_eq G y₂ x).choose_spec]

Goal state after:
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 : Surjective ⇑f
x y : G'
⊢ f (x⁻¹ * y) = (f x)⁻¹ * f y

Tactic:
rw [f.map_mul, f.map_inv]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (map L.subtype (comap L.subtype K)) ≠ 0

Tactic:
← relIndex_comap,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype (map L.subtype (comap L.subtype J))).relIndex (comap L.subtype K) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2

Tactic:
exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
· exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩

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

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x + y).cast = (↑x.cast + ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x + ↑y.cast).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x * y).cast = (↑x.cast * ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = (x * ↑y.cast).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x - y).cast = (↑x.cast - ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x - ↑y.cast).cast
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (h • J).relIndex (map ((MulDistribMulAction.toMonoidEnd H G) h) K) = J.relIndex K

Tactic:
← relIndex_comap,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (comap ((MulDistribMulAction.toMonoidEnd H G) h) (h • J)).relIndex K = J.relIndex K
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (h • J).relIndex (map ((DistribMulAction.toAddMonoidEnd H G) h) K) = J.relIndex K

Tactic:
← relIndex_comap,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (comap ((DistribMulAction.toAddMonoidEnd H G) h) (h • J)).relIndex K = J.relIndex K
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors

Tactic:
rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.properDivisors ↔ 1 < n

Tactic:
mem_properDivisors,

Goal state after:
n : ℕ
⊢ 1 ∣ n ∧ 1 < n ↔ 1 < n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
grw [← hx.le]
    gcongr
    simpa only [mul_one] using mul_lt_mul_of_neg_left ihn hx0

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
mem_properDivisors,

Goal state after:
p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∣ p ^ k ∧ x < p ^ k ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
rw [intCast_eq_intCast_iff_dvd_sub] at he

Goal state after:
n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k : ℕ
⊢ (Set.range fun n ↦ m * n + k) = {n | ↑n = ↑k ∧ k ≤ n}

Tactic:
by
  ext n
  simp only [Set.mem_range, Set.mem_ofPred_eq]
  conv => enter [1, 1, y]; rw [add_comm, eq_comm]
  refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  · simpa using congr_arg ((↑) : ℕ → ZMod m) ha
  · obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
    simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
    obtain ⟨b, rfl⟩ := H₁
    exact ⟨b, ha⟩

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

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

Tactic:
contrapose!
  exact digits_length_le_iff hb n

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

Goal state before:
pp: case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases le_or_gt b 1 with hb | hb

Goal state after:
case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))

Tactic:
assumption

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

Goal state before:
pp: case zero
b n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ l1.length = l2.length

Tactic:
assumption

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Tactic:
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
    exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a

Tactic:
assumption

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a

Tactic:
assumption

Goal state after:
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
key : x ^ (2 * (r + 1)) = x
⊢ x ^ n = x ^ (2 * ((r + 1) * n))

Tactic:
by rw [← mul_assoc, pow_mul, key]

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✝¹ : 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:
rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

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

Goal state before:
pp: case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1

pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
· 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])

Goal state after:
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = (n.choose k).factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [eq_comm]

Goal state after:
n k : ℕ
hkn : k ≤ n
⊢ ((n.choose k).factorization.prod fun x1 x2 ↦ x1 ^ x2) = ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p
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.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [eq_comm]

Goal state after:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ Nat.card G = 1

Tactic:
pow_card_eq_one'

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑g ^ Nat.card (G ⧸ H) = 1

Tactic:
pow_card_eq_one'

Goal state after:
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
assumption

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
rw [divByMonic, dif_pos hq, dif_pos hq, dif_pos h, mul_add, sub_add_eq_sub_sub]

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

Goal state before:
pp: case inr
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 : ¬g.IsRoot (eval r X ^ p ^ n)
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
← eval_pow,

Goal state after:
case inr
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 : ¬g.IsRoot (eval r (X ^ p ^ n))
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
a✝¹ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y _x →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p✝ : R[X]
x✝¹ : p✝ ≠ 0
a✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p✝, x✝¹⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
x✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun p x ↦ p.natDegree) y ⟨p, hp⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree
⊢ ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree

Tactic:
assumption

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((⇑derivative)^[k + 1] p).coeff m = (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1)

Tactic:
by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (C.comp f) r * eval₂ (C.comp f) X p = f r • eval₂ (C.comp f) X p

Tactic:
RingHom.comp_apply,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ C (f r) * eval₂ (C.comp f) X p = f r • eval₂ (C.comp f) X p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
← p.modByMonic_add_div (X - C a)

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
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)).natDegree < n

Tactic:
natDegree_divByMonic p (monic_X_sub_C a),

Goal state after:
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.natDegree - (X - C a).natDegree < n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative)^[m + 1] p

Tactic:
rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff

Tactic:
leadingCoeff_add_of_degree_lt,

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (q * (p /ₘ q)).leadingCoeff

R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_right]

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

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
exact ⟨a₀, ha₀s, fun a ha => all_top a ha (f a₀)⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ n.descFactorial n • (X - C c) ^ (n - n) = ↑n !

Tactic:
n.sub_self,

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ n.descFactorial n • (X - C c) ^ 0 = ↑n !
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ ∀ (a : α), Irreducible a ↔ Prime a

Tactic:
apply UniqueFactorizationMonoid.irreducible_iff_prime

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (f - single i 1 + single i 1).sum fun i c ↦ c • w i

Tactic:
sum_add_index',

Goal state after:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = ((f - single i 1).sum fun i c ↦ c • w i) + (single i 1).sum fun i c ↦ c • w i

case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ {x | p.IsRoot x}.Finite

Tactic:
simpa only [← Finset.setOfPred_mem, Multiset.mem_toFinset, mem_roots hp]
    using p.roots.toFinset.finite_toSet

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

Goal state before:
pp: case pos
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 ∈ nthRootsFinset n (f a)

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 ∈ nthRootsFinset n (f a)

Tactic:
· simp [hn] at hx

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 ∈ nthRootsFinset n (f a)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
n : ℕ
s : Set α
⊢ n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
by
  classical
  induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

Goal state after: