mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.hxy
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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

Goal state before:
pp: case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

Tactic:
rw [digits_zero]
        rfl

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

Goal state before:
pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
digits_getLast n (le_add_left 2 b)

Goal state after:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 2).digits (n / (b + 2))).getLast ?neg.q✝ ≠ 0

case neg.q
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ (b + 2).digits (n / (b + 2)) ≠ []
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
n : ℕ
⊢ multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
by
  simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ ∃ n, 0 < n ∧ y ^ n = 1

Tactic:
exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩

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 : ℕ
hx✝ : IsOfFinOrder x
hpos : 0 < ⋯.choose
hx : x ^ ⋯.choose = 1
⊢ Group ↥(powers x)

Tactic:
exact Submonoid.groupPowers hpos hx

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
ext L

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1)!.factorization p = (n + 1).factorization p + n !.factorization p

Tactic:
rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]

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

Goal state before:
pp: case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

Tactic:
simp [zero_dvd_iff.mp h]

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
⊢ 2 * p + (k % p + (n - k) % p) < succ 2 * p

Tactic:
two_mul,

Goal state after:
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
⊢ p + p + (k % p + (n - k) % p) < succ 2 * p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
two_mul,

Goal state after:
case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ n + n - n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False

Tactic:
apply pa.ne_one

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
apply (mul_right_cancel_iff (a := x ^ m)).1

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ k * x ^ m = 1 * x ^ m
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
calc
        x ^ k * x ^ m = x ^ (k + m) := (pow_add _ _ _).symm
        _ = x ^ (m + k) := by simp [Nat.add_comm]
        _ = x ^ m := h
        _ = 1 * x ^ m := by simp

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

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

Tactic:
simp only [of'_apply, coeff_divOf, add_comm a, coeff_mul_single_add, mul_one]

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

Goal state before:
pp: 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
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
this : n ∣ a.factorization p
⊢ a.factorization p = (n • factors) p

Tactic:
by
    simp [factors, Nat.mul_div_cancel' this]

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

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

Tactic:
· exact Or.inr (h_add hp hq)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
⊢ X ^ n ∣ f

Tactic:
induction n with
    | zero => simp [pow_zero]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]

Goal state after:
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
⊢ ↑0 < ↑p.natDegree

Tactic:
← degree_eq_natDegree hp0

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
⊢ ↑0 < p.degree
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p %ₘ q = p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p /ₘ q = 0

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p /ₘ q = 0
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
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by
        have := Nontrivial.of_polynomial_ne hp0
        rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
          degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
        exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
    div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
        calc
          _ ≤ degree (p %ₘ q) := degree_map_le
          _ < degree q := degree_modByMonic_lt _ hq
          _ = _ :=
            Eq.symm <|
              degree_map_eq_of_leadingCoeff_ne_zero _
                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this✝ : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
| p

Tactic:
rw [← modByMonic_add_div p 1]

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

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ i ∈ cons n.succ (Ioc n.succ p.natDegree) ⋯, a ^ (i - (n + 1)) * p.coeff i =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i

Tactic:
sum_cons,

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ a ^ (n.succ - (n + 1)) * p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
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, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

pp: case succ.e_a.refine_2
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)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
· rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      lia

Goal state after:
case succ.e_a.refine_2
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)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ {If | If.fst.Finite ∧ ∀ (i : ↑If.fst), True}.Countable

Tactic:
refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ {If | If.fst.Finite ∧ ∀ (i : ↑If.fst), True} ⊆ range (Sigma.map SetLike.coe fun x ↦ id)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n m : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - m) ∣ (⇑derivative)^[m] p

Tactic:
induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    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: case a
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p ∣ p

Tactic:
apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x q ∣ q

Tactic:
apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
l : (i : ι) → Filter (β i)
⊢ (pi fun i ↦ comap (f i) (l i)) = comap (Pi.map f) (pi l)

Tactic:
by
  simp [Filter.pi, Filter.comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ ⊤ ×ˢ g = comap Prod.snd g

Tactic:
rw [prod_eq_inf, comap_top, top_inf_eq]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ ∂ a = a

Tactic:
by rw [boundary, h, inf_top_eq]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → β
inst✝ : Zero β
⊢ Tendsto f cofinite (pure 0) ↔ HasFiniteSupport f

Tactic:
simp [Function.HasFiniteSupport, Function.support]

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

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

Tactic:
rw [coprod_eq_prod_top_sup_top_prod]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∃ p, a ~ᵤ p ∧ f = {p}

Tactic:
have := Classical.decEq α
  refine @Multiset.induction_on _
    (fun g => (g.prod ~ᵤ a) → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = {p}) f ?_ ?_ pfa.2 pfa.1
  · intro h; exact (ha.not_isUnit (associated_one_iff_isUnit.1 (Associated.symm h))).elim
  · rintro p s _ ⟨u, hu⟩ hs
    use p
    have hs0 : s = 0 := by
      by_contra hs0
      obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0
      apply (hs q (by simp [hq])).2.1
      refine (ha.isUnit_or_isUnit (?_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left ?_
      · rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
          mul_comm, mul_comm p _, mul_assoc]
        simp
      apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)
      apply (hs p (Multiset.mem_cons_self _ _)).2.1
    simp only [mul_one, Multiset.prod_cons, Multiset.prod_zero, hs0] at *
    exact ⟨Associated.symm ⟨u, hu⟩, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 2 r = 0 ↔ ¬∃ r_1, r = r_1 ^ 2

Tactic:
eq_zero_iff_forall_notMem,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ r_1, r = r_1 ^ 2
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ p
⊢ Irreducible x

Tactic:
exact hp x h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ^ 2 - C 1 = (X + C 1) * (X - C 1)

Tactic:
simp [← sq_sub_sq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ normalize 0 = 0

Tactic:
normalize_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ IsRelPrime a b

Tactic:
intro p p_dvd_a _
      exact isUnit_of_dvd_unit p_dvd_a a_unit

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
p q : R[X]
hq : q = 0
⊢ (p / q).degree ≤ p.degree

pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
· simp [hq]

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ (X - C (f a)) ^ rootMultiplicity (f a) (map f p) ∣ map f p

Tactic:
apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
· simp [hq]

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y✝ : Associates D[X] := Associates.mk f
hy : y✝ ≠ 0
H : Type (max 0 u) := { x // x ∣ y✝ }
hfin : Fintype H := fintypeSubtypeDvd y✝ hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
x y : G
heq : i x = i y
⊢ x = y

Tactic:
rw [Subtype.mk.injEq] at heq ⊢

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y✝ : Associates D[X] := Associates.mk f
hy : y✝ ≠ 0
H : Type (max 0 u) := { x // x ∣ y✝ }
hfin : Fintype H := fintypeSubtypeDvd y✝ hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
x y : G
heq : Associates.mk ↑x = Associates.mk ↑y
⊢ ↑x = ↑y
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count (a * b).factors

Tactic:
rw [count_mul ha hb hp, hb0, add_zero]

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors

Tactic:
apply Or.intro_right
    rw [ha0, zero_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q : R[X]
⊢ ∃ c, ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d

Tactic:
rcases exists_primitive_lcm_of_isPrimitive p.isPrimitive_primPart
        q.isPrimitive_primPart with
      ⟨r, rprim, hr⟩
    refine ⟨C (lcm p.content q.content) * r, fun s => ?_⟩
    by_cases hs : s = 0
    · simp [hs]
    by_cases hpq : C (lcm p.content q.content) = 0
    · rw [C_eq_zero, lcm_eq_zero_iff, content_eq_zero_iff, content_eq_zero_iff] at hpq
      rcases hpq with (hpq | hpq) <;> simp [hpq, hs]
    iterate 3 rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]
    nontriviality R
    rw [(associated_content_mul ..).dvd_iff_dvd_left, rprim.content_eq_one, mul_one, content_C,
      (associated_primPart_mul (mul_ne_zero hpq rprim.ne_zero)).dvd_iff_dvd_left, rprim.primPart_eq,
      normalize_lcm, lcm_dvd_iff,
      (isUnit_primPart_C (lcm p.content q.content)).mul_left_dvd, ← hr s.primPart]
    tauto

Goal state after: