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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * 4 ^ n < 4 * (n * n.centralBinom)

Tactic:
gcongr

Goal state after:
case hbc
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
⊢ p ^ k ∣ n ↔ k ≤ a

Tactic:
subst hab
  cases Nat.lt_or_ge a k with
  | inl hlt =>
    refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd
    exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd
  | inr hle =>
    refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle
    exact Nat.pow_dvd_pow p hle

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

Goal state before:
pp: p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
by
  obtain rfl | hp₁ : p = 0 ∨ 1 < p := by grind
  · rcases k.eq_zero_or_pos with rfl | hk <;> simp [Nat.ne_of_gt, *]
  · exact pow_dvd_iff_le_of_spec hp₁ hn (pow_padicValNat_mul_divMaxPow p n)
      (not_dvd_divMaxPow hp₁ hn)

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n

Tactic:
intro h₂

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
h₂ : multiplicity a b = n
⊢ emultiplicity a b = ↑n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
rw [multiplicity, emultiplicity_eq_top.mpr h]
  decide

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → ¬x ^ m = 1

Tactic:
← isPeriodicPt_mul_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : a ≤ b
⊢ x ^ a = x ^ b

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle

Goal state after:
case inl
G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ x ^ a = x ^ (a + c)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : b ≤ a
⊢ x ^ a = x ^ b

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ x ^ (b + c) = x ^ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b

Tactic:
gcongr

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Tactic:
← isPeriodicPt_mul_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ↔ IsPeriodicPt (fun x ↦ y * x) n 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n : ℕ
x✝¹ : 0 ≤ n
x✝ : 0 ≠ 0
⊢ n.factorization p ≤ (n.choose 0).factorization p + (factorization 0) p

Tactic:
by tauto

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
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
this : 3 ≤ p
⊢ 3 * p ≤ p * p

Tactic:
gcongr

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

Goal state before:
pp: case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ ((n + 1) * n !).factorization p = 0

Tactic:
factorization_mul n.succ_ne_zero n.factorial_ne_zero,

Goal state after:
case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (n.succ.factorization + n !.factorization) p = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD 0]
⊢ n = m

Tactic:
Nat.modEq_zero_iff

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n = m
⊢ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ n ≡ m [MOD 0] ↔ n = m

Tactic:
Nat.modEq_zero_iff

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ n = m ↔ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ y ^ k • a = a

Tactic:
← MulAction.toPerm_apply,

Goal state after:
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm (y ^ k)) a = a
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 = 0

Tactic:
← one_pow p

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 ^ p = 0
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ emultiplicity p n ! ≤ ↑(n / (p - 1))

Tactic:
rw [hp.emultiplicity_factorial (lt_succ_self _)]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) ≤ ↑(n / (p - 1))
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:
rw [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₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ then 1 else 0) = 0

Tactic:
if_neg (mt (congr_arg Nat.succ) H.symm),

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ n * 1 ≤ n * p

Tactic:
gcongr

Goal state after:
case h₂
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 1 ≤ p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inl
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' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)

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✝ : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
· rw [h']

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

Tactic:
rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]

Goal state after:
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 ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
⊢ derivativeFinsupp (C r) = Finsupp.single 0 (C r)

Tactic:
by
  ext i : 1
  match i with
  | 0 => simp
  | i + 1 => simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ derivative (p ^ (n + 1) * p) = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
derivative_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ derivative (p ^ (n + 1)) * p + p ^ (n + 1) * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n * r)

Tactic:
derivative_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n) * r + q ^ n * derivative r
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i) → ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Tactic:
simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), ∃ t, (∀ (i_1 : p ↑i), s ↑i ⊆ t i_1) ∧ V i = ⋂ (i : p ↑i), t i) ∧ t = ⋂ i, V i) →
    ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q

Tactic:
gcongr

Goal state after:
case a
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p ∣ p

case a
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x q ∣ q
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
derivative_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n)) * q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n * X)) * derivative q
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
⊢ derivative (f i ::ₘ Multiset.map f s).prod =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) (i ::ₘ s)).sum

Tactic:
Multiset.prod_cons,

Goal state after:
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
⊢ derivative (f i * (Multiset.map f s).prod) =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) (i ::ₘ s)).sum
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
⊢ derivative (f i * (Multiset.map f s).prod) =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) (i ::ₘ s)).sum

Tactic:
derivative_mul,

Goal state after:
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
⊢ derivative (f i) * (Multiset.map f s).prod + 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)) (i ::ₘ s)).sum
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
⊢ (mapDomain f ⁻¹' {x}).Finite

Tactic:
let e : s ↪ α := Function.Embedding.subtype (fun u ↦ u ∈ s)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
⊢ (mapDomain f ⁻¹' {x}).Finite
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h
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
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
      match
        match a, ha with
        | (T, i), x => (T.erase i, i) with
      | (T, i) => ∏ a ∈ T, (X - C a)

pp: case hi
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
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a, ha with
      | (T, i), x => (T.erase i, i)) ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match x with
        | (T, i) => i ∉ T}

pp: case hj
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
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match a, ha with
      | (T, i), x => (insert i T, i)) ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match x with
        | (T, i) => i ∈ T}

Tactic:
all_goals grind

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

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset M₀
hm : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}
hprod : m.prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
induction m using Multiset.induction generalizing x y with

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

Goal state before:
pp: case cons
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
⊢ a * s.prod ∣ a * k

Tactic:
gcongr

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
⊢ s.prod ∣ k
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✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False

Tactic:
rw [← one_smul R (w s)] at h

Goal state after:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ False
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ degree f = ∑ i, f i

Tactic:
degree_apply,

Goal state after:
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∑ i ∈ f.support, f i = ∑ i, f i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case a
α : 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 α := ⋯
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ p ::ₘ fx, Irreducible x

Tactic:
exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)

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

Goal state before:
pp: 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
this : Nontrivial α
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map normalize (a ::ₘ s)

Tactic:
Multiset.prod_cons,

Goal state after:
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
this : Nontrivial α
⊢ normalizedFactors (a * s.prod) = Multiset.map normalize (a ::ₘ s)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
⊢ p ∈ normalizedFactors x

Tactic:
obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd

Goal state after:
case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p ∈ normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ normalizedFactors m.prod = m

Tactic:
obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx

Goal state after:
case inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
h✝ : Subsingleton α
h : ∀ p ∈ 0, Prime p
⊢ normalizedFactors (Multiset.prod 0) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x → ¬IsUnit x

pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x

Tactic:
· intro h hx
    obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
    exact
      (prime_of_normalized_factor _ hp).not_isUnit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)

Goal state after:
case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x