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

Goal state before:
pp: a b c : ℕ
h : b ∣ c
hb : b ≠ 0
hc : c ≠ 0
⊢ b.factorization a ≤ c.factorization a

Tactic:
by
  obtain ⟨k, rfl⟩ := h; simp [factorization_mul hb (Nat.ne_zero_of_mul_ne_zero_right hc)]

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

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p

Tactic:
div_add_mod,

Goal state after:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p

Tactic:
div_add_mod,

Goal state after:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k + (n - k) < succ 2 * p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k

Tactic:
conv_rhs => rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]

Goal state after:
n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = (n.choose k).factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

Tactic:
simp only [one_pow, pow_one]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, (n + k) / p ^ i) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + (↑(∑ i ∈ Ico 1 b, k / p ^ i) + emultiplicity p n !)

Tactic:
hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)),

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ↑(∑ i ∈ Ico 1 b, (n + k) / p ^ i) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + (↑(∑ i ∈ Ico 1 b, k / p ^ i) + ↑(∑ i ∈ Ico 1 b, n / p ^ i))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n ≡ m [ZMOD 0]
⊢ n = m

Tactic:
Int.modEq_zero_iff

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n = m
⊢ n = m
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)

Tactic:
by
    rw [← hp.emultiplicity_mul]
    refine emultiplicity_le_emultiplicity_of_dvd_right ?_
    rw [← add_one_mul_choose_eq]
    exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 1) x = x ^ p

Tactic:
iterateFrobenius_def,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p ^ 1 = x ^ p
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 0) x = x

Tactic:
iterateFrobenius_def,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p ^ 0 = x
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

Tactic:
iterateFrobenius_def,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p ^ (m + n) = (x ^ p ^ n) ^ p ^ m
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (_root_.frobenius S p) ((algebraMap R S) r * s) =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s

Tactic:
map_mul,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (_root_.frobenius S p) ((algebraMap R S) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (_root_.iterateFrobenius S p n) (f • s) =
    (_root_.iterateFrobenius R p n) f • (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
iterateFrobenius_def,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (f • s) ^ p ^ n = f ^ p ^ n • (↑↑(_root_.iterateFrobenius S p n)).toFun s
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

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

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
intro n a _
    by_cases a0 : a = 0
    · exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
    · refine Or.inr ?_
      rw [C_mul_X_pow_eq_monomial]
      exact h_monomial a0 n.succ_ne_zero

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
⊢ (f - g).coeff n = a - b

Tactic:
subst hf hg

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ (expand R p) ((expand R q) (C r * X ^ (n + 1))) = (expand R (p * q)) (C r * X ^ (n + 1))

Tactic:
map_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ (expand R p) ((expand R q) (C r)) * (expand R p) ((expand R q) (X ^ (n + 1))) =
    (expand R (p * q)) (C r) * (expand R (p * q)) (X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
map_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r) * (expand R 1) (X ^ (n + 1)) = C r * X ^ (n + 1)
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 a * f + contract p b * g = 1

Tactic:
← contract_mul_expand hp,

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 (a * (expand R p) f) + contract p (b * (expand R p) g) = 1
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
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))

Tactic:
rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),

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
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a (X - C x) + rootMultiplicity a (p /ₘ (X - C x))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) ((X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g))

Tactic:
map_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) ((X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f) * (expand R (p ^ n)) g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0

Tactic:
simpa [Monic.def.1 hg]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ coeff 0 n = 0

pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.degree < (X - C a).degree

Tactic:
coeff_zero

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ 0 = 0

case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.degree < (X - C a).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < (X - C a).degree

Tactic:
degree_X_sub_C

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0

Tactic:
rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < (X - C a).degree

Tactic:
degree_X_sub_C

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
have : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

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

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)

Tactic:
by
  obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) := by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc
  have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)
  let x : ℕ → { i : ι' // p i } := fun n =>
    Nat.recOn n (hs.index _ <| this 0) fun n xn =>
      hs.index _ <| inter_mem (this <| n + 1) (hs.mem_of_mem xn.2)
  have x_anti : Antitone fun i => s (x i).1 :=
    antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans inter_subset_right
  have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
    rintro (_ | i)
    exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]
  refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩
  have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti
  convert! this
  exact
    le_antisymm (le_iInf fun i => le_principal_iff.2 <| by cases i <;> apply hs.set_index_mem)
      (hx'.symm ▸
        le_iInf fun i => le_principal_iff.2 <| this.1.mem_iff.2 ⟨i, trivial, x_subset i⟩)

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

Goal state before:
pp: case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ - p₂ %ₘ q

Tactic:
simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ - p₁ %ₘ q

Tactic:
simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)

Tactic:
rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi))
    with ⟨k₀, hk₀, hk₀'⟩

Goal state after:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
k₀ : κ
hk₀ : p k₀
hk₀' : s k₀ ⊆ ⋂ i ∈ I, s (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
by_cases h : p = 0

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

case neg
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree
Module: Mathlib.Order.Filter.Prod

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

Tactic:
by
  simp only [prod_eq_inf, comap_iInf, inf_iInf]

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

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

Tactic:
Function.iterate_one,

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ derivative ((⇑derivative)^[k] (∏ a ∈ S, (X - C a))) =
    ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0

Tactic:
exact h (hw s)

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ n = 0

Tactic:
rw [smul_eq_zero, or_iff_not_imp_right] at h
    exact h (hw s)

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

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

Tactic:
have ha : a ≠ 0 := h.ne_zero_iff.mpr hb

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
ha : a ≠ 0
⊢ (factors a).card = (factors b).card
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
| Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) p.roots

Tactic:
rw [← p.map_roots_comp_C_mul_X_add_C a b ha]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
| Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) (Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
⊢ (C r * p).content = normalize r * p.content

Tactic:
by_cases h0 : r = 0; · simp [h0]
  rw [content, content, ← Finset.gcd_mul_left]
  refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
by_cases h : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
by_cases h : p = 0

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

case neg
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
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
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
⊢ rootMultiplicity t (derivative p) = m - 1

Tactic:
have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt

Goal state after:
case neg
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
⊢ rootMultiplicity t (derivative p) = m - 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i ↦ f.coeff ↑i
⊢ Set.InjOn π fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
        exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = C p.content * p.primPart

Tactic:
by_cases h : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * p.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.IsPrimitive

Tactic:
by_cases h : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive
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 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

Tactic:
refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩

Goal state after:
case pos.refine_1
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
⊢ p * c' * a' = p * a

case pos.refine_2
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
⊢ p * c' * b' = p * b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card ↑(Set.range f) = #(image f univ)

Tactic:
by rw [← Set.toFinset_card, Set.toFinset_range]

Goal state after: