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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (l ++ [0]) = ofDigits b l

Tactic:
rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ (↑n)⁻¹.val) ^ n = a

Tactic:
by
  replace hn : (Nat.card α).Coprime n := hn
  rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]

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

Goal state before:
pp: p n : ℕ
⊢ n.divMaxPow p * p ^ padicValNat p n = n

Tactic:
unfold divMaxPow padicValNat

Goal state after:
p n : ℕ
⊢ (p.maxPowDvdDiv n).snd * p ^ (p.maxPowDvdDiv n).fst = n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b

pp: case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b

Tactic:
· exact digits_lt_base hb hi

Goal state after:
case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
· rw [hb.multiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

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

Goal state before:
pp: case mp
n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n → n = 0 ∨ ¬p ∣ n

pp: case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n

Tactic:
· intro h
    by_cases n_zero : n = 0
    · simp [n_zero]
    · right
      rw [← h]
      exact not_dvd_ordCompl hp n_zero

Goal state after:
case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
simpa [pa] using h a

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

Goal state before:
pp: case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
⊢ Prime p → d.factorization p ≤ n.factorization p

Tactic:
pp

Goal state after:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ d.factorization p ≤ n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
rw [← div_eq_one] at hab ⊢

Goal state after:
G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a / (fun a ↦ a ^ n) b = 1
⊢ a / b = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 = 0

Tactic:
← one_pow (p ^ n)

Goal state after:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1

Tactic:
by
  rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]

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

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Tactic:
simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 1 < ↑1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
degree_add_eq_left_of_degree_lt this

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun e a ↦ C a * (X ^ p) ^ e).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = if p ∣ n then f.coeff (n / p) else 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rcases p.eq_zero_or_pos with hp | hp
  · rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
  by_cases hf : f = 0
  · rw [hf, map_zero, natDegree_zero, zero_mul]
  have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]
  refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
  · rw [coeff_expand hp]
    split_ifs with hpn
    · 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
    · rfl
  · refine le_degree_of_ne_zero ?_
    rw [coeff_expand_mul hp, ← leadingCoeff]
    exact mt leadingCoeff_eq_zero.1 hf

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

Goal state before:
pp: case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
intro _

Goal state after:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
⊢ n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree →
    (if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).2
        else p).degree <
      q.degree

Tactic:
rw [dif_pos hq, if_neg h]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (0, p).2.degree < q.degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
⊢ (¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)) → f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
nex

Goal state after:
case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 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
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))).divModByMonicAux hq).1 =
    p -
      (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) +
        q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1)

Tactic:
sub_add_eq_sub_sub

Goal state after:
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))).divModByMonicAux hq).1 =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1
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:
← isRoot_comp,

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.comp (X ^ p ^ n)).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
expand_eq_C hp

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = 0

Tactic:
simp only [h0, natDegree_zero]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) p = 0

Tactic:
rw [← aeval_map_algebraMap A, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ 0 ∈ Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
⊢ (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)

Tactic:
induction n with
  | zero =>
    simp [Finset.range]
  | succ n IH =>
    calc
      derivative^[n + 1] (p * q) =
          derivative (∑ k ∈ range n.succ,
              n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
        rw [Function.iterate_succ_apply', IH]
      _ = (∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
          ∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) := by
        simp only [Nat.succ_eq_add_one, nsmul_eq_mul, derivative_mul, derivative_natCast, zero_mul,
          derivative_sum, zero_add, Function.iterate_succ', Function.comp_apply]
        simp_rw [mul_add, sum_add_distrib]
      _ = (∑ 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 • (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) := by
        rw [add_comm, add_assoc]
      _ = (∑ i ∈ range n.succ,
              (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
            1 • (derivative^[n + 1] p * derivative^[0] q) := by
        simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
      _ = ∑ k ∈ range n.succ.succ,
            n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
        rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
    congr
    refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
    · 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
    · rw [Nat.choose_zero_right, tsub_zero]

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

Goal state before:
pp: case h
α : 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 : ↑I
hpi : p ↑i
⊢ s ↑i ⊆ t i hpi

Tactic:
exact ht₁ i hpi

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

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
biInter_eq_iInter,

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ i ∈ s, g i
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False

Tactic:
← one_smul R (w s)

Goal state after:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ False
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:
rw [sum_add_index', sum_single_index, one_smul, weight_apply]

Goal state after:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

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.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0

Tactic:
intro _

Goal state after:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ (0 ^ (n + 1)).roots = (n + 1) • roots 0

Tactic:
rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Subsingleton α
⊢ ∀ (x : α), x ∉ s

Tactic:
intro _

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Subsingleton α
x✝ : α
⊢ x✝ ∉ s
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
← Nat.cast_le (α := WithBot ℕ)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
by
  by_cases hn : n = 0
  · simp [hn] at hx
  · rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val

Tactic:
have h : (X * p).support = p.support.map ⟨Nat.succ, Nat.succ_injective⟩ := by
    ext a
    simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]
    rcases a with - | a
    · simp
    rw [mul_comm, coeff_mul_X]
    constructor
    · intro h
      use a
    · rintro ⟨b, ⟨h1, h2⟩⟩
      rw [← Nat.succ_injective h2]
      apply h1

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ X.content = 1

Tactic:
← mul_one X,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ (X * 1).content = 1
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
n : ℕ
⊢ (X ^ n).aroots S = n • {0}

Tactic:
by
  rw [aroots_pow, aroots_X]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ image f univ ⊆ p.roots.toFinset

Tactic:
intro _

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x✝ : R
⊢ x✝ ∈ image f univ → x✝ ∈ p.roots.toFinset
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) = gcd a q.content

Tactic:
rw [content_eq_gcd_range_of_lt q (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_right _ _) (Nat.lt_succ_self _))]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ ↑(normUnit p) = C ↑(normUnit p.leadingCoeff)

Tactic:
by
  simp [normUnit]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ factors' a = factors' b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ~ᵤ 0
⊢ factors' a = factors' 0

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ factors' a = factors' b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0

Tactic:
simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]
  exact factors_eq_top_iff_zero.not

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ (Associates.mk a).factors

Tactic:
factors_mk _ hz

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk a

Tactic:
apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ a ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots

Tactic:
simp [roots_degree_eq_one h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ a.degree < a.degree + ↑c.natDegree

Tactic:
Polynomial.degree_eq_natDegree ane0,

Goal state after:
case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ ↑a.natDegree < ↑a.natDegree + ↑c.natDegree