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

Goal state before:
pp: case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
intro b

Goal state after:
case refine_2
h2 : _root_.Prime 2
b : Bool
⊢ ∀ (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * single g 1 %ᵒᶠ g).coeff g' = 0

Tactic:
rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_mul_single_of_forall_add_ne]
    simpa [eq_comm, add_comm] using h

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

Goal state before:
pp: case succ
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n

Tactic:
rw [Finset.range_add_one, Finset.filter_insert]

Goal state after:
case succ
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * if n = 0 then 0 else X ^ (n - 1)).natDegree = n - 1

Tactic:
split_ifs with n0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case succ
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n

Tactic:
rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : ℤ
⊢ (↑a).coeff n = ↑(if n = 0 then a else 0)

Tactic:
by
  simp only [← C_eq_intCast, coeff_C, Int.cast_ite, Int.cast_zero]

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

Goal state before:
pp: case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

Tactic:
intro b

Goal state after:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
⊢ b ∈ f.support → b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ ((expand R p) f).coeff n = 0

Tactic:
coeff_expand hp

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Tactic:
intro b

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)

Tactic:
rw [map_add, eval_add, eval_add, hf, hg]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 /ₘ p = 0

Tactic:
by
  grind [divByMonic, divModByMonicAux]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ n) = C ↑n * X ^ (n - 1)

Tactic:
convert! derivative_C_mul_X_pow (1 : R) n

Goal state after:
case e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = C 1 * X ^ n

case e'_3
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 1 * ↑n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p

Tactic:
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
      mul_pow, ← C.map_pow, frobenius_def]

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < ↑q.natDegree + (p /ₘ q).degree

Tactic:
degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((⇑derivative)^[k + 1] p).coeff m = (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1)

Tactic:
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ (aeval ((algebraMap A B) x)) p = (algebraMap A B) ((aeval x) p)

Tactic:
rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: 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)
⊢ (⇑derivative)^[n + 1] (p * q) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))

Tactic:
rw [Function.iterate_succ_apply', IH]

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

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated

Tactic:
h.1.eq_iInf

Goal state after:
case mpr
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
⊢ (⨅ i, f i).IsCountablyGenerated

Tactic:
choose s hs using fun i => exists_antitone_basis (f i)

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ (⨅ i, f i).IsCountablyGenerated
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (↑n * (f ^ (n - 1) * derivative f)))

Tactic:
iterate_derivative_natCast_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c (↑n * (⇑derivative)^[m] (f ^ (n - 1) * derivative f))
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_3
α : Type u_2
f : Filter α
⊢ f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2

Tactic:
← Filter.hnot_def,

Goal state after:
case refine_3
α : Type u_2
f : Filter α
⊢ f = ￢￢f ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
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
  simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
    hp.exists_mem_multiset_dvd h

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

Goal state before:
pp: case insert
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]

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

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

Tactic:
Multiset.countP_pos

Goal state after:
case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1 ∈ s, a ~ᵤ a_1
⊢ False
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:
induction s using Multiset.induction_on generalizing n with
  | empty => simp only [Multiset.prod_zero, one_dvd]
  | cons a s induct =>
    rw [Multiset.prod_cons]
    obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
    gcongr
    refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
    have a_prime := h a (Multiset.mem_cons_self a s)
    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
    refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
    have assoc := b_prime.associated_of_dvd a_prime b_div_a
    have := uniq a
    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
    exact this ⟨b, b_in_s, assoc.symm⟩

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
          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.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p * q ≠ 0
r : R
⊢ count r (p * q).roots = count r (p.roots + q.roots)

Tactic:
rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]

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

Goal state before:
pp: case refine_2
σ : Type u_1
p : σ →₀ ℕ
⊢ p ∈ {d | degree d = 1} → p ∈ Set.range fun a ↦ single a 1

Tactic:
(hp : p.sum (fun a k ↦ k) = 1)

Goal state after:
case refine_2
σ : Type u_1
p : σ →₀ ℕ
hp : (p.sum fun a k ↦ k) = 1
⊢ p ∈ Set.range fun a ↦ single a 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx left✝ : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)

Tactic:
simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
      lt_add_iff_pos_right, normalizedFactors_pos, hc]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
p : S[X]
inst✝ : Algebra S R
h : Function.Injective ⇑(algebraMap S R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ (aeval x) p = 0

Tactic:
by
  classical
  exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
hnezero : derivative p ≠ 0
⊢ ¬(X - C t) ^ (m - 1 + 1) ∣ derivative p

Tactic:
hm

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
hnezero : derivative p ≠ 0
⊢ ¬(X - C t) ^ m ∣ derivative p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

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

Tactic:
obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b

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

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

Tactic:
intro b

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t

Tactic:
by
  simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]

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

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

Tactic:
exact (natDegree_eq_of_degree_eq_some <| degree_eq_one_of_irreducible_of_root hirr <|
    isRoot_of_mem_roots hx).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h : ↑sa ≤ b.factors
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h_sb : b.factors = ↑sb
⊢ p.count ↑sa ≤ p.count b.factors

Tactic:
h_sb

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ↑sa ≤ ↑sb
h_sb : b.factors = ↑sb
⊢ p.count ↑sa ≤ p.count ↑sb
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a.factors.prod

Tactic:
← ha',

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ (Associates.mk a0).factors
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ (Associates.mk a0).factors.prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
by_cases hp0 : p = 0
  · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]
  exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq]

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

Goal state before:
pp: case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ p.count a.factors

Tactic:
exact eq_pow_count_factors_of_dvd_pow hp h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ -(aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
dvd_neg,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ (aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
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:
convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1

Goal state after:
case e'_3
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
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

case convert_2
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
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (algebraMap K L) 0
Module: Mathlib.Data.DFinsupp.Small

Goal state before:
pp: ι : Type u
π : ι → Type v
inst✝³ : (i : ι) → Zero (π i)
σ : Type u_1
R : Type u_2
inst✝² : Zero R
inst✝¹ : Small.{u, u_2} R
inst✝ : Small.{u, u_1} σ
⊢ Small.{u, max u_2 u_1} (σ →₀ R)

Tactic:
by
  classical
  exact small_map finsuppEquivDFinsupp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ RingHom.ker ((↑(map f (AlgHom.id R D))).comp ↑(map (AlgHom.id S A) g)) =
    Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)

Tactic:
rw [← RingHom.comap_ker]

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.comap (↑(map (AlgHom.id S A) g)) (RingHom.ker ↑(map f (AlgHom.id R D))) =
    Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)