mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g

Tactic:
rw [RingEquiv.coe_ringHom_inj_iff]
    apply RingHom.ext_zmod _ _

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

Goal state before:
pp: case succ.zero.succ
n : ℕ
ih : ofDigits (0 + 1) ((0 + 1).digits n) = n
⊢ ofDigits (0 + 1) ((0 + 1).digits (n + 1)) = n + 1

Tactic:
rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]

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

Goal state before:
pp: p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
x✝ : a < k ∨ a ≥ k
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
cases Nat.lt_or_ge a k with

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

Goal state before:
pp: case zero
m : ℕ
hb : 1 < 0
⊢ m ≠ 0 → 0 ^ (digits 0 m).length ≤ 0 * m

Tactic:
simp_all [base_pow_length_digits_le']

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

Goal state before:
pp: case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m ≠ 0 → (0 + 1) ^ ((0 + 1).digits m).length ≤ (0 + 1) * m

Tactic:
simp_all [base_pow_length_digits_le']

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

Goal state before:
pp: case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Tactic:
simp_all [base_pow_length_digits_le']

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬a ^ k ∣ b

Tactic:
hf.pow_dvd_iff_le_multiplicity,

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬k ≤ multiplicity a b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ ↑n.natAbs = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
zpow_natCast

Goal state after:
case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ ↑n.natAbs = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
zpow_natCast

Goal state after:
case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ ↑(multiplicity a b) ≤ ↑(multiplicity c d) ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
← hab.emultiplicity_eq_multiplicity,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ emultiplicity a b ≤ ↑(multiplicity c d) ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
this.emultiplicity_eq_multiplicity

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = ↑(multiplicity p b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y

Tactic:
rw [← orderOf_pos_iff] at hx ⊢; exact Nat.pos_of_dvd_of_pos h hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
by
            rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy
            simp [hy, pow_add, mul_comm, mul_left_comm]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b * b ^ (l - 1)

Tactic:
← Nat.pow_succ',

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b ^ (l - 1).succ
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
this : a = 1
⊢ orderOf x = n

Tactic:
simp [this, ha]

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ d.factorization p ≤ n.factorization p

Tactic:
factorization_eq_zero_of_not_prime _ hp

Goal state after:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
p : ℕ
hp : ¬Prime p
⊢ 0 ≤ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / n)) = n

Tactic:
rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : (n / d * d).factorization p < n.factorization p
⊢ False

Tactic:
factorization_mul h1 hd,

Goal state after:
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : ((n / d).factorization + d.factorization) p < n.factorization p
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

Tactic:
by
  refine ⟨factorization_div, ?_⟩
  rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n); · simp
  have h1 : n / d ≠ 0 := by simp [*]
  intro h
  rw [dvd_iff_le_div_mul n d]
  by_contra h2
  obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)
  rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ x ^ i = 1 ↔ x ^ ↑i = 1

Tactic:
zpow_natCast

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ x ^ i = 1 ↔ x ^ i = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
x : G
⊢ IsOfFinOrder x ↔ IsUnit x

Tactic:
by
  use IsOfFinOrder.isUnit
  rintro ⟨u, rfl⟩
  rw [Units.isOfFinOrder_val]
  apply isOfFinOrder_of_finite

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ x ^ ↑w = 1

Tactic:
zpow_natCast

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ x ^ w = 1
Module: Mathlib.Algebra.Polynomial.Inductions

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

Tactic:
divX_C,

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

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

Tactic:
sum

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
⊢ p * r = p * C (p * r).leadingCoeff

Tactic:
obtain rfl | hr := eq_or_ne r 0

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
hdeg : (p * 0).natDegree ≤ p.natDegree
⊢ p * 0 = p * C (p * 0).leadingCoeff

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ p * r = p * C (p * r).leadingCoeff
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
⊢ p %ₘ 0 = p

Tactic:
by
    have := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X) = C a

Tactic:
by
  simp [C_mul_X_eq_monomial, mul_one]

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
⊢ p /ₘ 0 = 0

Tactic:
by
    have := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0

Tactic:
| _ _ ih
   => 

Goal state after:
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
rcases B.eq_empty_or_nonempty with hB | Bnonempty

Goal state after:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ p.degree = 1

Tactic:
by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ f = ⊥

Tactic:
simpa [funext_iff] using coprodᵢ_neBot_iff.not

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

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

Tactic:
exact Or.inr fun ha => hnab ⟨ha, hb⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ derivative (eval₂ C q p₁) + derivative (eval₂ C q p₂) = eval₂ C q (derivative (p₁ + p₂)) * derivative q

Tactic:
ih₁,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ eval₂ C q (derivative p₁) * derivative q + derivative (eval₂ C q p₂) = eval₂ C q (derivative (p₁ + p₂)) * derivative q
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' (s + t) = ⇑ofAdd '' s * ⇑ofAdd '' t

Tactic:
← Set.image2_add,

Goal state after:
M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' Set.image2 (fun x1 x2 ↦ x1 + x2) s t = ⇑ofAdd '' s * ⇑ofAdd '' t
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' Set.image2 (fun x1 x2 ↦ x1 + x2) s t = ⇑ofAdd '' s * ⇑ofAdd '' t

Tactic:
Set.image_image2_distrib ofAdd_add,

Goal state after:
M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ Set.image2 HMul.hMul (⇑ofAdd '' s) (⇑ofAdd '' t) = ⇑ofAdd '' s * ⇑ofAdd '' t
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) S).prod) = (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
by
  nth_rw 1 [← Multiset.cons_erase hr]
  have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
  simpa using this

Goal state after:
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
ha0 : a = 0
⊢ p ∣ a ∨ p ∣ b

Tactic:
by simp [ha0]

Goal state after:
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
hb0 : b = 0
⊢ p ∣ a ∨ p ∣ b

Tactic:
by
          simp [hb0]

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

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

Tactic:
obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem

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 ::ₘ 0).prod = Multiset.map normalize (a ::ₘ 0)

case cons.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map normalize s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ b ∈ s, Irreducible b
b : α
hb : b ∈ s
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map normalize (a ::ₘ s)
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
induction n with
  | zero => rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
  | succ n ihn =>
    rcases eq_or_ne p 0 with (rfl | hp)
    · rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
    · rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
⊢ (factors a).card ≤ {b}.card

Tactic:
rw [card_factors_of_irreducible ha, Multiset.card_singleton]

Goal state after:
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 : ↑(#S) = p.degree
⊢ p ≠ 0

Tactic:
by contrapose! hcard; simp [hcard]

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

Goal state before:
pp: case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b p : R
⊢ p ∣ a → p ∣ b → IsUnit p

Tactic:
p_dvd_a

Goal state after:
case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
⊢ p ∣ b → IsUnit p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).natDegree

Tactic:
rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a = b.factors.prod
⊢ a = b

Tactic:
factors_prod

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a = b
⊢ a = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
factors_prod

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors = (a * b).factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a ≤ b.factors.prod
⊢ a ≤ b

Tactic:
factors_prod

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a ≤ b
⊢ a ≤ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
⊢ a.prod ≤ b.prod ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, prod_mono⟩
  have : a.prod.factors ≤ b.prod.factors := factors_mono h
  rwa [prod_factors, prod_factors] at this

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
hq' : q.leadingCoeff ≠ 0
⊢ (p % q).natDegree < q.natDegree

Tactic:
rw [mod_def]

Goal state after:
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).natDegree < q.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count (a * b).factors

Tactic:
count_mul ha hb hp,

Goal state after:
case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count a.factors + p.count b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors

Tactic:
count_mul ha hb hp,

Goal state after:
case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count a.factors + p.count b.factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Tactic:
← lift_id #R[X]

Goal state after:
R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ x⁻¹ = -((aeval x) p.divX / (algebraMap K L) (p.coeff 0))

Tactic:
by
  convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
  · rw [aeval_eq, zero_sub, div_neg]
  rw [RingHom.map_zero]
  convert! aeval_eq
  conv_rhs => rw [← divX_mul_X_add p]
  rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)) = -((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)

Tactic:
neg_mul

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)) = -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX))