mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ 2 ^ n

Tactic:
by
  obtain (rfl | hn) := eq_zero_or_pos n
  · cases k <;> simp
  · exact (Nat.choose_lt_two_pow _ _ hn).le

Goal state after:
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
induction n using Nat.strong_induction_on with | _ n IH

Goal state after:
case h
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
a : ℕ
ha : n = k + a
⊢ ∃ y, n = k + m * y

Tactic:
simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁

Goal state after:
case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₂ : k ≤ n
a : ℕ
ha : n = k + a
H₁ : m ∣ a
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1

Tactic:
induction n using Nat.strong_induction_on with | _ n IH

Goal state after:
case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
by
  simp [h.emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
ha : FiniteMultiplicity a 1
⊢ multiplicity a 1 = 0

Tactic:
by
  simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False

Tactic:
← pow_zero x

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f a ^ n ∣ f b

Tactic:
rw [← map_pow]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f (a ^ n) ∣ f b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
by
  simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range b)).PairwiseDisjoint fun d ↦ consFixedLengthDigits hb l d

Tactic:
by
  refine Finset.pairwiseDisjoint_iff.mpr fun i _ j _ ⟨L, hL⟩ ↦ ?_
  rw [Finset.mem_inter] at hL
  exact (consFixedLengthDigits_head hb hL.1).symm.trans (consFixedLengthDigits_head hb hL.2)

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).biUnion (consFixedLengthDigits hb l)

Tactic:
Finset.mem_biUnion,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a ∈ Finset.range b, L ∈ consFixedLengthDigits hb l a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p

Tactic:
simp [hp.factorization]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1

Tactic:
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
  · rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
  · rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers hx).symm ((Equiv.setCongr ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩

Tactic:
exact finEquivPowers_symm_apply _ n

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (n + 1)

Tactic:
by
  rw [add_comm]; cases p; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (f + g).coeff (n✝ * p) = f.coeff (n✝ * p) + g.coeff (n✝ * p)

Tactic:
coeff_add

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

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

Tactic:
← eq,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
have h : natDegree (C r) < natDegree (X - C a) := by simp

Goal state after:
case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ t ∈ ⨅ i, l i

Tactic:
grw [← hsub]

Goal state after:
case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ∈ ⨅ i, l i
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ↑I) → ι' ↑i
hsub : ⋂ i, s (↑i) (⟨I, f⟩.snd i) ⊆ t
hI : ⟨I, f⟩.fst.Finite
hf : ∀ (i : ↑⟨I, f⟩.fst), p (↑i) (⟨I, f⟩.snd i)
⊢ t ∈ ⨅ i, l i

Tactic:
grw [← hsub]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ↑I) → ι' ↑i
hsub : ⋂ i, s (↑i) (⟨I, f⟩.snd i) ⊆ t
hI : ⟨I, f⟩.fst.Finite
hf : ∀ (i : ↑⟨I, f⟩.fst), p (↑i) (⟨I, f⟩.snd i)
⊢ ⋂ i, s (↑i) (⟨I, f⟩.snd i) ∈ ⨅ i, l i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

Tactic:
sInter_eq_biInter,

Goal state after:
α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
⊢ ⋂ i ∈ s, i ∈ f ↔ ∀ U ∈ s, U ∈ f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

Tactic:
by
  by_cases hp : p.natDegree = 0
  · simp [hp]
  rw [leadingCoeff, leadingCoeff, coeff_derivative, natDegree_derivative]
  norm_cast
  congr <;> lia

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:
rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ derivative ((X + C c) ^ m) = C ↑m * (X + C c) ^ (m - 1)

Tactic:
rw [derivative_pow, derivative_X_add_C, mul_one]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ i, f i).sets = (⨅ i, f i.down).sets

Tactic:
← Equiv.plift.surjective.iInf_comp,

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ x, f (Equiv.plift x)).sets = (⨅ i, f i.down).sets
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
replace hk' : n < k := by simpa [hkm] using hk'
    simp [Nat.choose_eq_zero_of_lt hk']

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

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

Tactic:
have hsum : derivative^[n] (p * X ^ m) =
      ∑ k ∈ range n.succ,
        (n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k)) := by
    simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]
    congr! 2 with k hk
    norm_cast
    ring
  rw [hsum]
  refine sum_congr_of_eq_on_inter (fun k hk hk' ↦ ?_) (by simp_all) (by simp)
  rcases le_or_gt k m with hkm | hkm
  · replace hk' : n < k := by simpa [hkm] using hk'
    simp [Nat.choose_eq_zero_of_lt hk']
  · simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_iInf, iInf_inf]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊓ b)

Tactic:
hnot_le_iff_codisjoint_right

Goal state after:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊓ b))
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 rw [EuclideanDomain.gcd_mul_lcm]; rfl

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:
classical
    exact
      Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
        (by simpa only [Multiset.map_id', Finset.mem_def] using div)
        (by
          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
            ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])

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
⊢ (Multiset.map normalize (Classical.choose ⋯)).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
← Associates.mk_eq_mk_iff_associated,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk (Multiset.map normalize (Classical.choose ⋯)).prod = Associates.mk (Classical.choose ⋯).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Tactic:
rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
    Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_add, h, ←
    Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd * tl.prod).roots = (↑(hd :: tl)).bind roots

Tactic:
roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2),

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ hd.roots + tl.prod.roots = (↑(hd :: tl)).bind roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: 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

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

Tactic:
· obtain rfl : s = 0 := by
      apply Multiset.eq_zero_of_forall_notMem
      intro _
      convert! hs
    simp

Goal state after:
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.RingTheory.UniqueFactorizationDomain.Basic

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

Tactic:
exact ⊤

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
simp only [h, map_zero, rootMultiplicity_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ p.count ↑s = Multiset.count ⟨p, hp⟩ s

Tactic:
by
  simp only [count, dif_pos hp, bcount]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : FactorSet α
h : p.prod = q.prod
⊢ p = q

Tactic:
unfold FactorSet at p q

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : WithTop (Multiset { a // Irreducible a })
h : prod p = prod q
⊢ p = q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ a✝¹ = a✝

Tactic:
← Multiset.map_eq_map Subtype.coe_injective

Goal state after:
case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ Multiset.map (fun a ↦ ↑a) a✝¹ = Multiset.map (fun a ↦ ↑a) a✝
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ C (f q.leadingCoeff⁻¹) * (map f p /ₘ (map f q * C (f q.leadingCoeff⁻¹))) =
    C (f q.leadingCoeff)⁻¹ * (map f p /ₘ (map f q * C (f q.leadingCoeff)⁻¹))

Tactic:
map_inv₀

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ C (f q.leadingCoeff)⁻¹ * (map f p /ₘ (map f q * C (f q.leadingCoeff)⁻¹)) =
    C (f q.leadingCoeff)⁻¹ * (map f p /ₘ (map f q * C (f q.leadingCoeff)⁻¹))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ a.factors ⊔ b.factors + a.factors ⊓ b.factors = (a * b).factors

Tactic:
factors_mul,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ a.factors ⊔ b.factors + a.factors ⊓ b.factors = a.factors + b.factors
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
hpm0 : ¬map f p = 0
⊢ ↑(map f p).roots.card ≤ p.degree

Tactic:
exact card_roots hpm0 |>.trans degree_map_le

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ Associated (p * q).primPart (p.primPart * q.primPart)

Tactic:
rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ Associated (p * q).primPart (p.primPart * q.primPart)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ (p * q).primPart = p.primPart * q.primPart

Tactic:
rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ (p * q).primPart = p.primPart * q.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : Nat.find h ≤ s.natDegree
⊢ False

Tactic:
rw [← rdeg] at hs

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
⊢ False
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ UniqueFactorizationMonoid (MvPolynomial σ D)

Tactic:
rw [iff_exists_prime_factors]

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ ∀ (a : MvPolynomial σ D), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors

Tactic:
have := nontrivial_of_ne _ _ hm

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ n * a).factors = n • a.factors + a.factors

Tactic:
factors_mul,

Goal state after:
case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ n).factors + a.factors = n • a.factors + a.factors
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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count (Associates.mk a0 * Associates.mk b0).factors =
    p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors

Tactic:
factors_mul,

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count ((Associates.mk a0).factors + (Associates.mk b0).factors) =
    p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : Algebra R S
p : R[X]
⊢ ((mapAlg R S) p).Monic ↔ p.Monic

Tactic:
simp [mapAlg_eq_map, monic_map_iff]

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ {x | IsAlgebraic R x}.Countable

Tactic:
← le_aleph0_iff_set_countable,

Goal state after:
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ #↑{x | IsAlgebraic R x} ≤ ℵ₀