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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
n✝ : ℕ
a✝ : ∀ {P : R[X]}, P.degree < ↑n✝ → (⇑derivative)^[n✝] P = 0
P : R[X]
h : P.degree < ↑(n✝ + 1)
⊢ (⇑derivative)^[n✝ + 1] P = 0

Tactic:
case succ k ind =>
    by_cases P = 0
    case pos hP => simp [hP]
    case neg hP =>
      rw [Function.iterate_add_apply, Function.iterate_one]
      by_cases derivative P = 0
      case pos hP' => simp [hP']
      case neg hP' =>
        have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
        refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
        linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
P : R[X]
h : P.degree < ↑k
⊢ (⇑derivative)^[k] P = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ (f ⁻¹' s).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ {b}.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ (f ⁻¹' {b}).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst✝¹ : TendstoCofinite g
inst✝ : TendstoCofinite f
r : ι
⊢ {b | b = r}.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst✝¹ : TendstoCofinite g
inst✝ : TendstoCofinite f
r : ι
⊢ (g ∘ f ⁻¹' {r}).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ TendstoCofinite _root_.id

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
u v : α → M
⊢ mapDomain f (u + v) = mapDomain f u + mapDomain f v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst✝² : AddCommMonoid M
inst✝¹ : TendstoCofinite f
inst✝ : DistribSMul R M
r : R
v : α → M
⊢ mapDomain f (r • v) = r • mapDomain f v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : i ∉ range f
⊢ mapDomain f v i = 0

Tactic:
by

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) S, derivative (∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - k) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
by

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) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) =
    ∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)

Tactic:
by

Goal state after:
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
y : α →₀ ℕ
hy : mapDomain f y = x
this : y.support ⊆ s
⊢ ↑y.support ⊆ range ⇑e

Tactic:
by

Goal state after:
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
y : α →₀ ℕ
hy : mapDomain f y = x
i : α
hi : ¬y i = 0
⊢ ¬y i = 0 ∧ f i = f i ∧ ¬y i = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
⊢ TendstoCofinite (mapDomain f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (gcd a b * lcm a b) (a * b)

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s : Multiset ι
f : ι → M₀
h : p ∣ (Multiset.map f s).prod
⊢ ∃ a ∈ s, p ∣ f a

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s : Multiset M₀
⊢ (∀ r ∈ 0, Prime r) → p ∣ Multiset.prod 0 → ∃ q ∈ 0, p ~ᵤ q

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
by

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
⊢ (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
    ∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)

Tactic:
by

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
⊢ (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a)

Tactic:
by

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:
by

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
⊢ (↑k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a) =
    ↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
⊢ derivative P = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : derivative P = 0
⊢ P ∣ derivative P

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
n : ℕ
chn : ↑n ≠ 0
a : R[X]
⊢ derivative (a ^ n) = 0 ↔ derivative a = 0

Tactic:
by

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

Goal state before:
pp: case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ k ∈ {r | IsUnit r ∨ Prime r}

pp: case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}

Tactic:
· left; exact .of_mul_eq_one_right _ hk

Goal state after:
case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
⊢ WellFounded DvdNotUnit

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
⊢ WfDvdMonoid α → WellFoundedLT (Associates α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ ∀ {a : Associates α}, Irreducible a ↔ Prime a

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s : σ
f : σ →₀ R
⊢ (weight (Pi.single s 1)) f = f s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
x : α
hx : x ∈ g
⊢ IsUnit g.prod

Tactic:
by

Goal state after:
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

Goal state after:
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✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ n = 0

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∈ p ::ₘ f

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
⊢ s.prod ∣ n

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p ↦ p) s.val, Prime a

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p ↦ p) s.val, a ∣ n

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : M₀), Multiset.countP (Associated a) (Multiset.map (fun p ↦ p) s.val) ≤ 1

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∏ p ∈ s, p ∣ n

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset M
⊢ (Multiset.map Associates.mk 0).prod = Associates.mk (Multiset.prod 0)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset M
a : M
s : Multiset M
ih : (Multiset.map Associates.mk s).prod = Associates.mk s.prod
⊢ (Multiset.map Associates.mk (a ::ₘ s)).prod = Associates.mk (a ::ₘ s).prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
q : α
hq : q ∈ f
⊢ q ∈ p ::ₘ f

Tactic:
by

Goal state after:
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 = (weight w) f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset (Associates M)
⊢ Multiset.prod 0 = 1 ↔ ∀ a ∈ 0, a = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset (Associates M)
⊢ ∀ (a : Associates M) (s : Multiset (Associates M)),
    (s.prod = 1 ↔ ∀ a ∈ s, a = 1) → ((a ::ₘ s).prod = 1 ↔ ∀ a_2 ∈ a ::ₘ s, a_2 = 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p * f.prod ~ᵤ b * (g.erase b).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p ∈ p ::ₘ f

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ (weight w) f

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod * 1 ≤ p.prod * (q - p).prod
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
⊢ p.prod ≤ q.prod

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
p : R[X]
inst✝ : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
⊢ ∀ {f g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s✝ : Multiset (Associates M₀)
p : Associates M₀
hp : Prime p
a : Associates M₀
s : Multiset (Associates M₀)
ih : p ≤ s.prod → ∃ a ∈ s, p ≤ a
h : p ≤ (a ::ₘ s).prod
⊢ p ≤ a * s.prod

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_3
M : Type u_4
inst✝ : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots.card ≤ p.natDegree

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = normalizedFactors x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
by

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 : R
hp0 : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
by

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 : R
hp0 : 0 < p.degree
h : p = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize a

Tactic:
by

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

Goal state before:
pp: R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
⊢ count a p.roots = rootMultiplicity a p

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ (weight w) f

Tactic:
by

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ ?m.50 ∉ p.roots

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p.IsRoot = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, Prime x

Tactic:
by

Goal state after: