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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
← natCast_val,

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1).val = ↑(n + 1) - 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Goal state after:
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
by
  rcases eq_or_ne m 0 with (rfl | hm); · simp [properDivisors]
  simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Goal state after:
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
⊢ a = b

Tactic:
rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.cast.val < m + 1

Tactic:
← natCast_val,

Goal state after:
case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ (↑a.val).val < m + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ 2 ∣ (n + 1).centralBinom

Tactic:
use (n + 1 + n).choose n

Goal state after:
case h
n : ℕ
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
h : AddSubgroup.zmultiples ↑n ≤ f.ker
⊢ f ↑n = 0

Tactic:
exact h (AddSubgroup.mem_zmultiples _)

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

Goal state before:
pp: case ind.succ.tail
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d < b + 2

Tactic:
· apply IH ((n + 1) / (b + 2))
    · apply Nat.div_lt_self <;> lia
    · assumption

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

Goal state before:
pp: case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
      rw [Nat.ofDigits_mod_eq_head! _ _]
      exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

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

Goal state before:
pp: n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ n = p ^ k

Tactic:
rw [← Nat.prod_factorization_pow_eq_self hn, h]

Goal state after:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ ((single p k).prod fun x1 x2 ↦ x1 ^ x2) = p ^ k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ orderOf x * y)

Tactic:
← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred.succ * y)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n

Tactic:
have hdisj : Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
        {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
      simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : Monoid G
x : G
n✝ m✝ : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
· rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n✝ m✝ : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
· rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = 0

Tactic:
Nat.card_eq_zero_of_infinite

Goal state after:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ 0 = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = 0

Tactic:
Nat.card_eq_zero_of_infinite

Goal state after:
case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ 0 = 0
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 n ih h
    by_cases hn : n = 0
    · subst hn
      simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
      simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]
      rw [Prime.emultiplicity_one]
      · exact zero_lt_one
      · decide
    have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) := by
      rw [prime_two.emultiplicity_factorial_mul]
      rw [two_mul]
      push_cast
      apply WithTop.add_lt_add_right _ (ih hn)
      exact Ne.symm nofun
    cases b
    · simpa
    · suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]
      rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
      refine this.trans ?_
      exact mod_cast lt_succ_self _

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Goal state after:
case inl
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
h : n ∣ k ^ 0
⊢ n.primeFactors ⊆ k.primeFactors

case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ k.primeFactors
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases hm0 : m = 0

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Semiring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha : IsOfFinOrder a
⊢ a = 1

Tactic:
by
  obtain ⟨n, hn, ha⟩ := ha.exists_pow_eq_one
  exact (pow_eq_one_iff_of_nonneg ha₀ hn.ne').1 ha

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

Goal state before:
pp: case inl
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hm : m ≠ 0
⊢ g ≠ 0

Tactic:
exact gcd_ne_zero_left hm

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

Goal state before:
pp: case pos
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
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : a = 0
⊢ (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

pp: case neg
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
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
· exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])

Goal state after:
case neg
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
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
C_mul_X_pow_eq_monomial,

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ ⊤ = p.trailingDegree + ⊤

Tactic:
add_top

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial n) a) = C (a * ↑n) * X ^ (n - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p

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 [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]

Goal state after:
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
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
⊢ (p /ₘ q).degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0
      rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
      exact WithBot.bot_lt_coe _

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⟩

Goal state after:
case mp.inter
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
by
  obtain ⟨r, rfl⟩ := dvd
  rw [derivative_mul, derivative_pow]
  exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
hsum

Goal state after:
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥

Tactic:
simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ

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

Goal state before:
pp: case cons.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ x * (y * k) ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]

Goal state after:
case cons.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ (k ::ₘ c ::ₘ s).prod ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod = x * (y * k)

Tactic:
rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]

Goal state after:
case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y ∨ k = 0
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}
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
by
  obtain ⟨m, hm, hprod⟩ := exists_multiset_of_mem_closure hxy
  induction m using Multiset.induction generalizing x y with
  | empty =>
    apply subset_closure
    push _ ∈ _
    simp only [Multiset.prod_zero] at hprod
    left; exact .of_mul_eq_one _ hprod.symm
  | cons c s hind =>
    simp only [Multiset.mem_cons, forall_eq_or_imp, Set.mem_ofPred] at hm
    simp only [Multiset.prod_cons] at hprod
    simp only [Set.mem_ofPred_eq] at hind
    obtain ⟨ha₁ | ha₂, hs⟩ := hm
    · rcases ha₁.exists_right_inv with ⟨k, hk⟩
      refine hind x (y * k) ?_ hs ?_
      · simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]
        refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure ?_,
          Multiset.forall_mem_cons.2 ⟨subset_closure ?_, fun t ht => subset_closure (hs t ht)⟩⟩)
        · left; exact .of_mul_eq_one_right _ hk
        · left; exact ha₁
      · rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
        left; exact hprod
    · rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩
      · rw [hc]; rw [hc, mul_assoc] at hprod
        refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
        · right; exact ha₂
        rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
        exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
      rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
      refine hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
      rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
      exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

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
⊢ b ∣ k

Tactic:
have a_prime := h a (Multiset.mem_cons_self a s)

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 ∣ k
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ p.IsRoot a ↔ ⊥ a

Tactic:
simp only [Pi.bot_apply, Prop.bot_eq_false, mem_roots hp0 |>.not.mp <| by simp [h]]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
⊢ s = 0

Tactic:
by_contra hs0

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
⊢ False
Module: Mathlib.Data.Finsupp.Weight

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

Tactic:
intro p (hp : p.sum (fun a k ↦ k) = 1)
    obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp
    use a

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X + C b).roots = {-(↑a⁻¹ * b)}

Tactic:
rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ k • {normalize p} = Multiset.replicate k (normalize p)

Tactic:
Multiset.nsmul_singleton

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ Multiset.replicate k (normalize p) = Multiset.replicate k (normalize p)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ n • {0} = replicate n 0

Tactic:
Multiset.nsmul_singleton

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ replicate n 0 = replicate n 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
n : ℕ
s : Set α
⊢ n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
n : ℕ
hη : 0 = a
⊢ False

Tactic:
exact ha hη.symm

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

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

Goal state after: