mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
by
  rw [isPrimePow_nat_iff_bounded_log]
  obtain rfl | h := eq_or_ne n 1
  · simp
  constructor
  · rintro ⟨k, hkle, hk_pos, p, hle, heq, hprime⟩
    refine ⟨k, hkle, hk_pos, ?_⟩
    rw [heq, hprime.pow_minFac hk_pos.ne']
  · rintro ⟨k, hkle, hk_pos, heq⟩
    refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
    · grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]
    · grind [Nat.minFac_prime_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : g₁ * g₂⁻¹ ∈ H
⊢ ⟨g₁ * g₂⁻¹, r⟩ • g₂ • b = g₁ • b

Tactic:
by simp [mul_smul]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ (fun m ↦ m • g₂⁻¹ • x) ⟨g₁⁻¹ * g₂, h⟩ = g₁⁻¹ • x

Tactic:
by simp [mul_smul]

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

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅

Tactic:
simpa using Prime.ne_one

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

Goal state before:
pp: n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList <+ k.primeFactorsList

Tactic:
obtain ⟨a, rfl⟩ := h
  exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Injective (Quotient.map' ⇑f ⋯)

pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
· simp_rw [← Quotient.eq''] at key
    refine Quotient.ind' fun x => ?_
    refine Quotient.ind' fun y => ?_
    exact (key x y).mpr

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (map f H).index ∣ H.index

Tactic:
by
  rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_one]
  exact index_dvd_of_le le_sup_left

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H

Tactic:
exact bot_le

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

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a % 0

Tactic:
Int.emod_zero,

Goal state after:
case zero
a : ℤ
⊢ (↑a).cast = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

Tactic:
rw [Nat.cast_sub, Nat.cast_one]

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k
Module: Mathlib.Algebra.Polynomial.Cardinal

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #R[X] = max #R ℵ₀

Tactic:
by
  simp [(toFinsuppIso R).toEquiv.cardinal_eq]

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

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * (↑u)⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos.refl
n : ℕ
ilt : Fact (1 < n)
ih : val 0 ^ 0 < n → (0 ^ 0).val = val 0 ^ 0
h : val 0 ^ (0 + 1) < n
⊢ val 0 ^ 0 < n

Tactic:
simp [ilt.out]

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : Nontrivial G
⊢ n ≠ 1

Tactic:
by
  rintro rfl
  obtain ⟨x, hx⟩ := exists_ne (0 : G)
  exact hx <| by simpa using char_nsmul_eq_zero 1 x

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

Goal state before:
pp: p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
obtain rfl | hp1 : p = 1 ∨ 1 < p := by grind

Goal state after:
case inl
n k : ℕ
hp : 1 ≠ 0
⊢ (1 ^ k * n).divMaxPow 1 = n.divMaxPow 1

case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
· have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

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

Goal state before:
pp: case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
← Nat.mul_sub

Goal state after:
case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length

Tactic:
(simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)

Goal state after:
case zero
b n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ l1.length = l2.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length

Tactic:
(simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)

Goal state after:
case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ emultiplicity a b

Tactic:
Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity,

Goal state after:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ ↑(multiplicity a b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ Nat.find h1 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
rw [find_eq_iff]

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ ((n > 0 ∧ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1) ∧ ∀ n_1 < n, ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 ↦ x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a = min (emultiplicity p a) (emultiplicity p b)

Tactic:
min_eq_left

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a = emultiplicity p a

case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a = min (multiplicity p a) (multiplicity p b)

Tactic:
min_eq_left

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a = multiplicity p a

case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
⊢ ∃ m, x ^ n = x ^ (2 * m)

Tactic:
have key : x ^ (2 * (r + 1)) = x := by
    have h2 : 2 * (r + 1) = 2 * r + 1 + 1 := by omega
    rw [h2, pow_succ, hx, one_mul]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
key : x ^ (2 * (r + 1)) = x
⊢ ∃ m, x ^ n = x ^ (2 * m)
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
    obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h
    simp [pow_add, pow_mul, hx]

Goal state after:
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
    obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h
    simp [pow_add, pow_mul, hx]

Goal state after:
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
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})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n

Tactic:
card_Ico 1 n.succ

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})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n.succ - 1
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
by
  simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n

Tactic:
card_Ico 1 n.succ

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n.succ - 1
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (C (p.coeff 0) + C a).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree

Tactic:
← C_add,

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (C (p.coeff 0 + a)).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inl.inl
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)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (C (p.coeff 0) + C (q.coeff 0)).natDegree = 0

Tactic:
← C_add,

Goal state after:
case refine_2.inl.inl
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)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (C (p.coeff 0 + q.coeff 0)).natDegree = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
rw [le_rootMultiplicity_iff hp]

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X ^ 2) = C (a * 2) * X

Tactic:
rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
by
  rw [← map_natCast C n]
  exact derivative_C

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

Goal state before:
pp: case inr
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 : ¬X - C (r ^ p ^ n) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd

Goal state after:
case inr
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)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp.univ
α : Type u
s : Set (Set α)
U : Set α
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ

Tactic:
exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩

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
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_seq x

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ (pi f).HasBasis (fun Ik ↦ Ik.1.Finite ∧ p Ik.2) fun Ik ↦ Ik.1.pi fun i ↦ s i Ik.2

Tactic:
refine hasBasis_pi h |>.to_hasBasis ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i : Set ι × (ι → κ)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
      ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)

case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i' : Set ι × κ),
    i'.1.Finite ∧ p i'.2 →
      ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ i'.1.pi fun i ↦ s i i'.2
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
map_equiv_symm,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ)) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
f' : Filter α
g' : Filter β
⊢ Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Tactic:
simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0

Tactic:
dsimp [normalizedFactors, factors]
    simp [Subsingleton.elim (1 : α) 0]

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

Goal state before:
pp: σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
⊢ f s ≤ degree f

Tactic:
by_cases h : s ∈ f.support
  · exact Finset.single_le_sum_of_canonicallyOrdered h
  · simp only [notMem_support_iff] at h
    simp only [h, zero_le]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x * x ^ n)) ((n + 1) • factors x)

Tactic:
succ_nsmul'

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

Tactic:
intro h
    obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h
    exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (r * (X ^ k).content) r

Tactic:
content_X_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (r * 1) r
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b

Tactic:
intro i _

Goal state after:
case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ p.content ∣ p.coeff i
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b

Tactic:
intro i _

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
a✝ : i ∈ p.support
⊢ r ∣ p.coeff i
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
hfR : ↑f.natDegree < #R
⊢ ∃ r, eval r f ≠ 0

Tactic:
by
  contrapose! hf
  exact eq_zero_of_forall_eval_zero_of_natDegree_lt_card f hf hfR

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q

Tactic:
← self_sub_C_mul_X_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ p * q - C (p * q).leadingCoeff * X ^ (p * q).natDegree - p.eraseLead * q
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ p * q - C (p * q).leadingCoeff * X ^ (p * q).natDegree - p.eraseLead * q

Tactic:
← self_sub_C_mul_X_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    p * q - C (p * q).leadingCoeff * X ^ (p * q).natDegree - (p - C p.leadingCoeff * X ^ p.natDegree) * q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ↑a✝ = ⊤

Tactic:
← FactorSet.prod_eq_zero_iff,

Goal state after:
case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ prod ↑a✝ = 0