mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False

Tactic:
simpa [hdiv] using FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
    (by by_contra! nh; simp [nh] at h) (lt_one_iff.mpr h)

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
· intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)

Tactic:
simp only [not_and_or, not_not] at hm ⊢

Goal state after:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L.head ⋯ = d

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
  rw [head_cons]

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

Goal state before:
pp: k m p : ℕ
hp : Prime p
⊢ p ^ k * m / p ^ (p ^ k * m).factorization p = m ↔ m = 0 ∨ ¬p ∣ m

Tactic:
by
  rw [ordCompl_self_pow_mul m k hp, ordCompl_eq_self_iff_zero_or_not_dvd m hp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
  exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

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

Goal state before:
pp: a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
this : ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) = a.gcd b
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

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

Tactic:
add_sub_assoc,

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

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finEquivPowers ⋯) ((finCongr h) ((finEquivPowers ⋯).symm ⟨x ^ n, ⋯⟩)) = ⟨y ^ n, ⋯⟩

Tactic:
finEquivPowers_symm_apply,

Goal state after:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finEquivPowers ⋯) ((finCongr h) ⟨n % orderOf x, ⋯⟩) = ⟨y ^ n, ⋯⟩
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
exact Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩

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

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
grw [← Nat.primeFactors_pow k hn, Nat.primeFactors_mono h <| pow_ne_zero n hk]

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
⊢ c ^ n ≠ 0

Tactic:
by simp [c, factors]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y

Tactic:
by
  rw [orderOf_eq_orderOf_iff]
  intro n
  exact (h.pow_right n).eq_one_iff

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

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : a ^ (m' * g) = b ^ (n' * g)
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'

Tactic:
rw [pow_mul, pow_mul] at h

Goal state after:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ (expand R p) f = (expand R ?p) (C r) ↔ f = (expand R ?p) (C r)

pp: case p
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ ℕ

Tactic:
expand_inj hp,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ f = C r ↔ f = (expand R p) (C r)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
· rw [hq, mul_zero, trailingDegree_zero, add_top]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
· rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
    apply WithTop.coe_add

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ⋯
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))

Tactic:
have := rootMultiplicity_comp_C_mul_X_add_C_le
    (p.comp (C a * X + C b)) ⅟a (- ⅟a * b) (a * c + b) (isUnit_of_invertible ⅟a)

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this✝ : Invertible a := ha.invertible
this :
  rootMultiplicity (a * c + b) ((p.comp (C a * X + C b)).comp (C ⅟a * X + C (-⅟a * b))) ≤
    rootMultiplicity (⅟a * (a * c + b) + -⅟a * b) (p.comp (C a * X + C b))
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this✝ : Invertible a := ha.invertible
this :
  rootMultiplicity (a * c + b) ((p.comp (C a * X + C b)).comp (C ⅟a * X + C (-⅟a * b))) ≤
    rootMultiplicity (⅟a * (a * c + b) + -⅟a * b) (p.comp (C a * X + C b))
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))

Tactic:
simpa [comp_assoc, mul_add, ← mul_assoc, ← map_mul] using this

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

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

Tactic:
dif_neg h

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p = p
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
dif_neg h

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h✝ : IsUnit p
u : R
h : C u = p
⊢ False

Tactic:
apply not_le.mpr (zero_lt_one' (WithBot ℕ))

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h✝ : IsUnit p
u : R
h : C u = p
⊢ 1 ≤ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ derivative (X + C c) = 1

Tactic:
by
  rw [derivative_add, derivative_X, derivative_C, add_zero]

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

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

Tactic:
induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_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
⊢ map f (r • p) = f r • map f p

Tactic:
by
  rw [map, eval₂_smul, RingHom.comp_apply, C_mul']

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p ≠ 0
Module: Mathlib.Order.Filter.CountablyGenerated

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

Tactic:
refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩

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

Goal state before:
pp: α : Type u_2
f g : Filter α
⊢ (f ⊔ g).ker = f.ker ∪ g.ker

Tactic:
← sSup_pair,

Goal state after:
α : Type u_2
f g : Filter α
⊢ (sSup {f, g}).ker = f.ker ∪ g.ker
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
nontriviality
  rcases hp.lt_or_gt with hd | hd
  · rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]
  refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_
  rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i ↦ id ((I, s).2 i)) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
  refine univ_pi_mem_pi (fun i ↦ ?_) ?_
  · by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]
  · filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
    simp [hiI, hsurj.range_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ((∃ x x_1, ↑x = ∅) ∨ ∃ x x, ↑x = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g

Tactic:
exists_const,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ ((∃ x, ↑x = ∅) ∨ ∃ x, ↑x = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Tactic:
simp only [Filter.coprod, mem_sup, compl_mem_comap]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) =
    (↑k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
rw [mul_sum]

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) =
    ∑ i ∈ powersetCard (#S - (k + 1)) S, (↑k + 1) * ∏ a ∈ i, (X - C a)
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✝ : Fintype σ
f : σ →₀ R
⊢ (weight w) f = ∑ i, f i • w i

Tactic:
by
  rw [weight_apply, f.sum_fintype (fun i c ↦ c • w i) fun _ ↦ zero_smul _ _]

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

Goal state before:
pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) f = 0

Tactic:
rw [h, map_zero]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : s = 0
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}

Tactic:
simp only [mul_one, Multiset.prod_cons, Multiset.prod_zero, hs0] at *

Goal state after:
case h
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
u : αˣ
a✝ : 1 ~ᵤ a → (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
hu : p * ↑u = a
hs : ∀ b ∈ p ::ₘ 0, Prime b
hs0 : True
⊢ a ~ᵤ p ∧ p ::ₘ 0 = {p}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ p.roots = S.val

Tactic:
refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ S.val ≤ p.roots

case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ p.roots.card ≤ S.val.card
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
x : α
hx : x ≠ 0
⊢ ∏ p ∈ (factors x).toFinset, p ^ count p (factors x) = (∑ a ∈ (factors x).toFinset, count a (factors x) • {a}).prod

Tactic:
by
    simp only [prod_sum, prod_nsmul, prod_singleton]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
have h : (C r).support = {0} := support_monomial _ h0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : (C r).support = {0}
⊢ (C r).support.gcd (C r).coeff = normalize r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (C ((algebraMap T S) a) * map (algebraMap T S) p).roots = p.aroots S

Tactic:
roots_C_mul

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (map (algebraMap T S) p).roots = p.aroots S

case ha
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
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'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')

Tactic:
by
  refine rootSet_maps_to' (fun h₀ => ?_) f
  obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])
  exact Polynomial.map_zero _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
| C (normalize r) * (C r).primPart

Tactic:
rw [← content_C, ← (C r).eq_C_content_mul_primPart]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
| C r
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ False

Tactic:
have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
⊢ ∀ (a_1 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0), a_1 ≍ a' → ↑(factors' a) ≍ ↑(factors' b)

Tactic:
exact fun ha hb _ => heq_of_eq <| congr_arg some <| factors'_cong hab

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

Goal state before:
pp: k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero

Goal state after:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Tactic:
simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝² : CommRing D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Finite σ
this : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (Fintype.card σ)) D)

Tactic:
induction Fintype.card σ with
    | zero =>
      apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid
      infer_instance
    | succ d hd =>
      apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid
      exact Polynomial.uniqueFactorizationMonoid

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

Goal state before:
pp: K : Type u_1
inst✝ : Ring K
f : K[X]
a : K
⊢ (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)

Tactic:
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : 1 ≤ (Associates.mk p).count (Associates.mk a).factors
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0

Tactic:
exact (zero_lt_one.trans_le h).ne'

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]
hp : p ≠ 0
q : R[X]
⊢ (gcd p q).degree ≤ p.degree

Tactic:
by
  have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)
  rwa [degree_eq_natDegree hp]

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental S B
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental R A

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)

Goal state after: