mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.succ.zero
R : Type u
inst✝ : Semiring R
a b : R
m : ℕ
⊢ (monomial (m + 1 + 0 - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + 0 - 1)) (a * (b * ↑0)) =
    (monomial (m + 1 - 1 + 0)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (0 - 1))) (a * (b * ↑0))

Tactic:
| zero =>

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

Goal state before:
pp: case neg
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
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have hf : f ≠ 0 := by
    intro hf
    apply hfg
    rw [hf, zero_divByMonic]

Goal state after:
case neg
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
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
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
⊢ ∀ (a : R), count a 0 = rootMultiplicity a p

Tactic:
intro a

Goal state after:
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
a : R
⊢ count a 0 = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (⇑derivative)^[0] (map f p) = map f ((⇑derivative)^[0] p)

Tactic:
| zero =>

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

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

Tactic:
| 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
⊢ 0 ∈ Multiset.map (⇑(aeval x) ∘ fun x ↦ X - C x) s

Tactic:
Multiset.mem_map

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
⊢ ∃ a ∈ s, (⇑(aeval x) ∘ fun x ↦ X - C x) a = 0
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
| zero =>

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

Goal state before:
pp: case mp.inter
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝
hW : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝

Tactic:
| inter _ _ hV hW =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
by
  rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

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

Goal state before:
pp: α : Type u_1
a : α
⊢ (pure a).IsCountablyGenerated

Tactic:
rw [← principal_singleton]

Goal state after:
α : Type u_1
a : α
⊢ (𝓟 {a}).IsCountablyGenerated
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (⇑derivative)^[0] (X ^ n) = ↑(n.descFactorial 0) * X ^ (n - 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (⇑derivative)^[0] ((X + C c) ^ n) = n.descFactorial 0 • (X + C c) ^ (n - 0)

Tactic:
| zero =>

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

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
· rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]
    exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥

Tactic:
by
  simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff]
    using! coprodᵢ_neBot_iff'.not

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)

Tactic:
eventually_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {x | p x} ∈ f ×ˢ 𝓟 s ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {x | p x} ∈ f ×ˢ 𝓟 s ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)

Tactic:
eventually_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {x | p x} ∈ f ×ˢ 𝓟 s ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set M
⊢ ⇑ofAdd '' (0 • s) = (⇑ofAdd '' s) ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
⊢ ⇑toAdd '' s ^ 0 = 0 • ⇑toAdd '' s

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ (⇑derivative)^[0] (p.comp (1 - X)) = (-1) ^ 0 * ((⇑derivative)^[0] p).comp (1 - X)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1 ∈ s, a ~ᵤ a_1
⊢ False

Tactic:
exact this ⟨b, b_in_s, assoc.symm⟩

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

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

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

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ Multiset.map f (p.comp (C a * X + C b)).roots = p.roots

Tactic:
rw [Multiset.ext]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ ∀ (a_1 : R), count a_1 (Multiset.map f (p.comp (C a * X + C b)).roots) = count a_1 p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : 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
q : α
hq : q ∈ s
⊢ a = p * ↑u * (s.erase q).prod * q

Tactic:
rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
          mul_comm, mul_comm p _, mul_assoc]

Goal state after:
case refine_1
α : 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
q : α
hq : q ∈ s
⊢ ↑u * (p ::ₘ s).prod = ↑u * (p * s.prod)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case zero
σ : Type u_5
f : σ →₀ ℕ
hn : 0 ≤ degree f
⊢ ∃ g ≤ f, degree g = 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ 0) = 0 • normalizedFactors x

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (p ^ 0).roots = 0 • p.roots

Tactic:
| zero =>

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors {a}.prod = Multiset.map normalize {a}

Tactic:
Multiset.prod_singleton,

Goal state after:
case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors a = Multiset.map normalize {a}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ fa.prod * fb.prod = (fa + fb).prod

Tactic:
by rw [Multiset.prod_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).prod.roots = s

Tactic:
rw [roots_multiset_prod, Multiset.bind_map]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s

Tactic:
Multiset.mem_map

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
⊢ normalizedFactors m.prod = m

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ normalizedFactors m.prod = m

case inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Subsingleton α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Nontrivial α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset 0 a₁
hη₂ : η₂ ∈ nthRootsFinset 0 a₂
⊢ η₁ * η₂ ∈ nthRootsFinset 0 (a₁ * a₂)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s✝ : Set α
s : Set (α →₀ ℕ)
⊢ ∀ (x y : Multiplicative (α →₀ ℕ)),
    { toFun := (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) ∘ ⇑Multiplicative.toAdd, map_one' := ⋯ }.toFun (x * y) =
      { toFun := (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) ∘ ⇑Multiplicative.toAdd, map_one' := ⋯ }.toFun x *
        { toFun := (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) ∘ ⇑Multiplicative.toAdd, map_one' := ⋯ }.toFun y

Tactic:
simp [Finsupp.prod_add_index, pow_add]

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset 0 a
⊢ False

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞

Tactic:
intro a

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
⊢ ℕ∞
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
p : T[X]
a : S
⊢ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
Polynomial.map_ne_zero_iff

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
p : T[X]
a : S
⊢ p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0

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
p : T[X]
a : S
⊢ Function.Injective ⇑(algebraMap T S)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ (X ^ 0).content = 1

Tactic:
| zero =>

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ aroots 0 S = 0

Tactic:
rw [← C_0, aroots_C]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
⊢ ∀ (a : β), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
⊢ ∀ (a : R), a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
intro a

Goal state after:
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b

Tactic:
intro a

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
⊢ IsUnit a → a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
intro a

Goal state after:
case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
⊢ ∀ (p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * (c' * b') = p * b

Tactic:
hb'

Goal state after:
case pos.refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * b = p * b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∑ i ∈ range m.succ,
      eval t (m.choose i • ((⇑derivative)^[m - i] ((X - C t) ^ m) * (⇑derivative)^[i] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

Tactic:
sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t (m.choose 0 • ((⇑derivative)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
p q : R[X]
hpq : (p * q).degree < ↑0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑0! ∈ nonZeroDivisors R

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
by_cases h : p = 0
  · rw [h, map_zero, rootMultiplicity_zero]
  exact derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝¹, Irreducible a

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a : Associates α
⊢ a ∈ Multiset.map Subtype.val a✝¹ → Irreducible a
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
⊢ False

Tactic:
rw [eq_C_of_degree_le_zero h] at hp0 hp

Goal state after:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : p.degree ≤ 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝, Irreducible a

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a : Associates α
⊢ a ∈ Multiset.map Subtype.val a✝ → Irreducible a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
⊢ p.roots = 0

Tactic:
by
  by_contra hroots
  have ⟨x, hx⟩ := exists_mem_of_ne_zero hroots
  exact hdeg <| natDegree_eq_of_degree_eq_some <|
    degree_eq_one_of_irreducible_of_root hirr (mem_roots'.mp hx).right

Goal state after: