mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
rw [List.append_assoc, ← digits_base_pow_mul hb hm]
  simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]
  ring

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : ∀ x ∈ l, x < b + 2
⊢ ofDigits (b + 2) l < (b + 2) ^ l.length

Tactic:
by
  induction l with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
congr

Goal state after:
case n
b b' : ℕ
h : b' % b = 1
n : ℕ
| b

case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
congr

Goal state after:
case n
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b

case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑(ofDigits b' (b'.digits n)) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
rw [coe_ofDigits]

Goal state after:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ofDigits (↑b') (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]
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:
by simp [this, ha]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
by
  unfold orderOf
  rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := contra

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := contra

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ ¬IsMulTorsionFree G ↔ ∃ a, a ≠ 1 ∧ IsOfFinOrder a

Tactic:
by
  simp [isMulTorsionFree_iff_not_isOfFinOrder]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}

Tactic:
congr

Goal state after:
case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = {x | x ^ n = 1}
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm

Goal state after:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
| b ^ (n' * g)
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0

Tactic:
split_ifs with h
  · subst h h_pow_bas
    exact coeff_pow_of_natDegree_le ‹_›
  · apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
    · exact natDegree_pow_le_of_le m ‹_›
    · exact Iff.mp ne_comm h

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ (eval₂ C 1 f).natDegree = 0

Tactic:
← C_1,

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ (eval₂ C (C 1) f).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
⊢ ∀ ⦃x₂ : ℕ × ℕ⦄, x₂ ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) x₂ → x = x₂

Tactic:
y

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
⊢ y ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y → x = y
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

Tactic:
intro x hx y hy eq

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
eq : (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y
⊢ x = y
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p 1 = 1

Tactic:
← C_1,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p (C 1) = C 1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = C 1

Tactic:
congr

Goal state after:
case e_6
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ ↑h.unit⁻¹ * (a - b) = 1
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)

Tactic:
exact absurd h' h

Goal state after:
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
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑(x ::ₘ t).card = ↑t.card + 1

Tactic:
congr

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
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ (x ::ₘ t).card = Add.add (↑t.card) 1
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
congr

Goal state after:
case succ.e_a
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k + 1] p * (⇑derivative)^[k] q) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
congr

Goal state after:
case succ.e_a.refine_1.e_a.e_a.e_a
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n - (k + 1) + 1 = n - k
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst✝ : DecidablePred fun n ↦ ¬(X - C a) ^ (n + 1) ∣ p
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
congr

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

Goal state before:
pp: case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
congr

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:
rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.coeff (p.natDegree - 1 + 1) * ↑(p.natDegree - 1 + 1) = p.coeff p.natDegree * ↑p.natDegree

Tactic:
congr

Goal state after:
case e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree

case neg.e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ ⋃ i, s i ∈ ⨆ i, f i

Tactic:
exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

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

Goal state before:
pp: ι : Sort u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
by
  refine ⟨exists_iInter_of_mem_iInf, ?_⟩
  rintro ⟨t, ht, rfl⟩
  exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p

Tactic:
rw [pow_zero]

Goal state after:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ Pairwise fun i j ↦ ∃ s t, Disjoint ↑s ↑t

Tactic:
simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

Tactic:
rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩

Goal state after:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∃ p_1, (∀ a ∈ s, p_1 a ∈ f a) ∧ ⋂ i, p i = ⋂ x, p_1 ↑x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
    simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
rcases all_top with ⟨y, hys, x, hx⟩
    have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
    simp only [not_le] at this
    obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
      exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩
    refine ⟨a₀, ha₀s, fun a has => (lt_or_ge (f a) x).elim ?_ (le_trans ha₀.le)⟩
    exact fun h => others_bigger a ⟨h, has⟩

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
congr

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ f i * derivative (Multiset.map f s).prod =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)

Tactic:
congr

Goal state after:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
simp [hP]

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

Goal state before:
pp: case e_f
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ normalize) x✝ = Associates.mk x✝

Tactic:
Function.comp_apply,

Goal state after:
case e_f
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ Associates.mk (normalize x✝) = Associates.mk x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ normalizedFactors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_normalizedFactors_of_dvd hx hp' hp'x

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ normalizedFactors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ normalizedFactors x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = {0}

Tactic:
← roots_X_sub_C,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = (X - C 0).roots
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
x✝ : α
⊢ normalize x✝ = (Associates.out ∘ Associates.mk) x✝

Tactic:
Function.comp_apply,

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ (C a * p).roots = p.roots

Tactic:
roots_C_mul _ ha

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ p.roots = p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ prod 0

Tactic:
rw [prod_zero]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
⊢ p ∣ a

Tactic:
by_cases hcases : a = 0
  · rw [hcases]
    exact dvd_zero p
  · exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (1 - C a).degree ≤ ↑0

Tactic:
← C_1,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (C 1 - C a).degree ≤ ↑0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : Associates α
hx : ¬x✝ = 0
x : Associates α
⊢ (⇑Associates.mkMonoidHom ∘ Classical.choose ⋯) x = id x

Tactic:
Function.comp_apply,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : Associates α
hx : ¬x✝ = 0
x : Associates α
⊢ Associates.mkMonoidHom (Classical.choose ⋯ x) = id x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ p.prod * c = p.prod * (factors c).prod

Tactic:
congr

Goal state after:
case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ c = (factors c).prod
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ content 1 = 1

Tactic:
← C_1,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ (C 1).content = 1
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 q : T[X]
hpq : p * q ≠ 0
this : map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
⊢ (map (algebraMap T S) (p * q)).roots = p.aroots S + q.aroots S

Tactic:
Polynomial.map_mul,

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
this : map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
⊢ (map (algebraMap T S) p * map (algebraMap T S) q).roots = p.aroots S + q.aroots S
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
Polynomial.map_mul,

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (map (algebraMap T S) (C a) * map (algebraMap T S) p).roots = p.aroots S
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
⊢ rootSet 1 S = ∅

Tactic:
← C_1,

Goal state after:
T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (C 1).rootSet S = ∅
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S') p = map (algebraMap T S') 0

Tactic:
rwa [Polynomial.map_zero]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
· rw [C_eq_zero, content_eq_zero_iff] at h
    simp [h]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
⊢ p.primPart.natDegree = p.natDegree