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

Goal state before:
pp: n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
Nat.eq_add_of_sub_eq hb rfl,

Goal state after:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ (b - 2 + 2).digits n = n % (b - 2 + 2) :: (b - 2 + 2).digits (n / (b - 2 + 2))
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case1
p✝ p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
hp₀ : 0 < p
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]

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

Goal state before:
pp: case succ.succ
m b : ℕ
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_

Goal state after:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ∀ (hm : n ≠ 0), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_

Goal state after:
case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b * ofDigits b L) % k

Tactic:
Nat.add_mod,

Goal state after:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d % k + b * ofDigits b L % k) % k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b' * ofDigits b' L) % k

Tactic:
Nat.add_mod,

Goal state after:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d % k + b' * ofDigits b' L % k) % k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ)[0]?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)

Tactic:
rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ n.succ % (b + 2) = n.succ / (b + 2) ^ default % (b + 2)
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 b

Tactic:
multiplicity_neg

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b = multiplicity p b
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:
multiplicity_neg

Goal state after:
α : 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
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 (a - b) = multiplicity p b

Tactic:
by
  rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt] <;> rw [multiplicity_neg]; assumption

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

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
intro x hx

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx : x ∈ d :: L
⊢ x < b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)

Tactic:
rintro ⟨d, hd₁, T, hT, rfl⟩

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd₁ : d < b
T : List ℕ
hT : T ∈ fixedLengthDigits hb l
⊢ d :: T ∈ fixedLengthDigits hb (l + 1)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [← factorization_le_iff_dvd hd hn]
  refine ⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩
  rwa [hprod, factorization_prod_pow_eq_self_of_le_factorization hle]

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by
  rw [← factorization_le_iff_dvd hd hn]
  refine ⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩
  rwa [hprod, factorization_prod_pow_eq_self_of_le_factorization hle]

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

Goal state before:
pp: case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
· simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp

Goal state after:
case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))
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 : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ m * x ^ k = x ^ m

Tactic:
by simp [hk]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n + k - k) / p ^ i +
        #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n + k - k) % p ^ i})) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n

Tactic:
by
      have hdisj :
        Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
          {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
        simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]
      rw [emultiplicity_choose hp hkn (lt_succ_self _),
        emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
          (lt_succ_of_le (log_mono_right hkn)),
        ← Nat.cast_add]
      apply WithTop.coe_mono
      rw [log_pow hp.one_lt, ← card_union_of_disjoint hdisj, filter_union_right]
      have filter_le_Ico := (Ico 1 n.succ).card_filter_le
        fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
      rwa [card_Ico 1 n.succ] at filter_le_Ico

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

Goal state before:
pp: case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < ↑(bit false n)

pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
· simpa

Goal state after:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
obtain ⟨c, hc⟩ := CharP.exists R
  have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
  obtain ⟨i, hi, rfl⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
  obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]
  assumption

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

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

Tactic:
rintro p q (hp | hp) (hq | hq)

Goal state after:
case refine_2.inl.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

case refine_2.inl.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

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)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).leadingCoeff

Tactic:
rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
hp : p ≠ 0
f : R →+* S
q : R[X]
n : ℕ
⊢ (map f (contract p q)).coeff n = (contract p (map f q)).coeff n

Tactic:
simp only [coeff_map, coeff_contract hp]

Goal state after:
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:
by
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
by
        rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp; exact hp rfl

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
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ 0 /ₘ g = 0

Tactic:
zero_divByMonic

Goal state after:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ 0 = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp.superset
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝ : GenerateSets s s✝
hVW : s✝ ⊆ t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝

Tactic:
exact ⟨t, hts, ht, htV.trans hVW⟩

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

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

Tactic:
by rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]

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

Tactic:
nth_rw 2 [← modByMonic_add_div p q]

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 = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (0 /ₘ (X - C a)).leadingCoeff = leadingCoeff 0

Tactic:
zero_divByMonic

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ leadingCoeff 0 = leadingCoeff 0
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
l₁ l₂ : Filter α
⊢ (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Tactic:
by
  simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map Prod.fst (f ×ˢ g) = f

Tactic:
ext s
  simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
    exists_mem_subset_iff]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i ↦ cofinite) ↔ sᶜ ∈ cofinite

Tactic:
by
    simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

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

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ ∀ (x : α), x ∉ f.ker

Tactic:
intro x hx

Goal state after:
case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
hx : x ∈ f.ker
⊢ False
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
⊢ (mapDomain f ⁻¹' {x}).Finite

Tactic:
refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
⊢ mapDomain f ⁻¹' {x} ⊆ embDomain e '' {f | degree f ≤ degree x}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
      exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), Prime x

Tactic:
intro x hx

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), normalize x = x

Tactic:
intro x hx

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ normalize x = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ ∀ x ∈ 0, Irreducible x

Tactic:
intro x hx

Goal state after:
case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
hx : x ∈ 0
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ ∀ x_1 ∈ normalizedFactors x + normalizedFactors y, Irreducible x_1

Tactic:
intro x hx

Goal state after:
case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx : x ∈ normalizedFactors x✝ + normalizedFactors y
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map normalize (factors a) = Multiset.map normalize (factors b)

Tactic:
h',

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (Associates.out ∘ Associates.mk) (factors a) = Multiset.map (Associates.out ∘ Associates.mk) (factors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
· exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)

Goal state after:
case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
⊢ p.IsPrimitive

Tactic:
rintro r ⟨q, h⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = C r * q
⊢ IsUnit r
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ (C r).content = normalize r

Tactic:
rw [content]
  by_cases h0 : r = 0
  · simp [h0]
  have h : (C r).support = {0} := support_monomial _ h0
  simp [h]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ (map (algebraMap T S) (p ^ n)).roots = n • p.aroots S

Tactic:
Polynomial.map_pow,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ (map (algebraMap T S) p ^ n).roots = n • p.aroots S
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : x ∈ p.rootSet S
⊢ f x ∈ p.rootSet S'

Tactic:
rw [mem_rootSet'] at hx ⊢
  rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
  exact ⟨mt hp hx.1, rfl⟩

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

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i ↦ map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p)) a b

Tactic:
Polynomial.map_pow,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i ↦ map (algebraMap R (FractionRing R)) (X - C i) ^ rootMultiplicity i p) a b