mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

Tactic:
refine left_of_add ?_ hn

Goal state after:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * n

Tactic:
mul_comm

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ n * minimalPeriod f^[n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)

Tactic:
← hM

Goal state after:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a) • m ^ (period m a * (n / period m a)) • a

Tactic:
pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a) • a
Module: Mathlib.Data.Finite.Sigma

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype α := Fintype.ofFinite α
this : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Finite ((a : α) × β a)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
⊢ n < (bs.insertIdx m x).length

Tactic:
rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
  simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
  rcases l with - | ⟨hd, tl⟩
  · simp at hn
  · have : (n + 1 + length tl) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]

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

Goal state before:
pp: M : Type u
inst✝³ : Monoid M
α : Type v
inst✝² : MulAction M α
β : Type u_1
inst✝¹ : MulAction M β
m : M
inst✝ : DecidableEq β
b : β
⊢ Decidable (m • b = b)

Tactic:
infer_instance

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
H : Subgroup G
inst✝¹ : Finite (orbitRel.Quotient G X)
inst✝ : Finite (G ⧸ H)
⊢ Finite ((ω : Quotient (orbitRel G X)) × orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω))

Tactic:
infer_instance

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

Goal state before:
pp: p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
mul_comm

Goal state after:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ H.relIndex K * K.index = H.index

Tactic:
mul_comm

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * H.relIndex K = H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ a ∈ K, a * g ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, b * g ∈ H ∨ b ∈ H

Tactic:
simp only [and_left_comm]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ a ∈ K, g * a ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, g * b ∈ H ∨ b ∈ H

Tactic:
simp only [and_left_comm]

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'
H : Subgroup G
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index

Tactic:
simp_rw [index, ← Nat.card_prod]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card ((G ⧸ H) × G' ⧸ K)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℤ
c : ℕ
⊢ a ≡ b [ZMOD ↑c] ↔ ↑c ∣ b - a

Tactic:
Int.modEq_iff_dvd

Goal state after:
a b : ℤ
c : ℕ
⊢ ↑c ∣ b - a ↔ ↑c ∣ b - a
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'
⊢ Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range

Tactic:
finite_iff_finite_and_finiteIndex f.ker,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Finite ↥f.ker ∧ f.ker.FiniteIndex ↔ Finite ↥f.ker ∧ Finite ↥f.range
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ (MulAction.toPermHom G (G ⧸ H)).ker.FiniteIndex

Tactic:
infer_instance

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

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

Goal state before:
pp: m n : ℕ
⊢ Nontrivial
    (match 0 with
    | 0 => ℤ
    | n.succ => Fin (n + 1))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors

Tactic:
by
  ext
  simp [Dvd.dvd, @eq_comm _ n (_ * _)]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b

Tactic:
mul_comm

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image (fun x ↦ n / x) n.divisors = n.divisors

Tactic:
by
  conv_rhs =>
    rw [← image_fst_divisorsAntidiagonal, ← map_div_left_divisors, map_eq_image, image_image]
  rfl

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

Goal state before:
pp: case mpr
⊢ Subsingleton (ZMod 1)

Tactic:
infer_instance

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

Goal state before:
pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ (n✝¹ + 1) * (n✝ + 1 + 1)

Tactic:
mul_comm

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ (n✝¹ + 1) * 2 ≤ (n✝¹ + 1) * (n✝ + 1 + 1)
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
mul_comm

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
⊢ b.digits 0 = []

Tactic:
rcases b with (_ | ⟨_ | ⟨_⟩⟩) <;> simp [digits, digitsAux0, digitsAux1]

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

Goal state before:
pp: p : ℕ
⊢ p.maxPowDvdDiv 0 = (0, 0)

Tactic:
by simp [maxPowDvdDiv]

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

Goal state before:
pp: p n : ℕ
h : ¬p ∣ n
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
cases n with
  | zero => simp at h
  | succ n => simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]

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

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
⊢ D :: L = L2

Tactic:
| cons D L ih =>

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
⊢ D :: L = L2
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 = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'

Goal state after:
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 = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
· simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b

Tactic:
by
  rw [← factorization_le_iff_dvd ha hb, Finsupp.le_def]
  congr! 1 with p
  obtain _ | _ | p := p <;> simp [Nat.pow_dvd_pow_iff_le_right]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (a * b).factorization

Tactic:
mul_comm

Goal state after:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (b * a).factorization
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p ((n + 1) * n !) = emultiplicity p n ! + emultiplicity p (n + 1)

Tactic:
hp.emultiplicity_mul,

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p (n + 1) + emultiplicity p n ! = emultiplicity p n ! + emultiplicity p (n + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
· exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp

Goal state after:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
· exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp

Goal state after:
case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1

Tactic:
hp.emultiplicity_mul,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
    emultiplicity p (n + 1) + 1
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})) + emultiplicity p (k ! * n !)

Tactic:
hp.emultiplicity_mul,

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})) + (emultiplicity p k ! + emultiplicity p n !)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (a * b).factorization p = b.factorization p

Tactic:
mul_comm

Goal state after:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (b * a).factorization p = b.factorization p
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

pp: case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
· 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

Goal state after:
case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Algebra.MonoidAlgebra.Division

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

Tactic:
rw [coeff_modOf_of_not_exists_add x _ _ h, coeff_single_mul_of_forall_add_ne, zero_add]

Goal state after:
case inr.h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), g + d ≠ g'
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
exact hp.bot_lt

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
r : R
⊢ contract p (C r) = C r

Tactic:
by simp [contract]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]), p = f * g → f.degree ≤ g.degree → IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g

Tactic:
mul_comm

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = g * f
this : ∀ (f g : R[X]), p = f * g → f.degree ≤ g.degree → IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ 0 < p.natDegree

Tactic:
exact hp.bot_lt

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ (x * p, y * p) = (p * x, p * y)

Tactic:
mul_comm

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ multiplicity (X - C x) (p * q) = multiplicity (X - C x) p + multiplicity (X - C x) q

Tactic:
multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ multiplicity (X - C x) p + multiplicity (X - C x) q = multiplicity (X - C x) p + multiplicity (X - C x) q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p

Tactic:
by
  simp only [rootMultiplicity, multiplicity, emultiplicity]
  split
  · rfl
  rename_i h
  simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]
  rw [untopD_coe_enat]
  congr

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
| p %ₘ ?m.80 + ?m.80 * (p /ₘ ?m.80)

pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ R[X]

Tactic:
(modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
| 0 + (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Tactic:
cases nonempty_fintype (PLift ι)

Goal state after:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]
  refine exists_congr fun i => ?_
  by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
have := neBot_of_le hle.1

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : f₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
  rfl

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ f.ker = ∅

Tactic:
by
  rw [le_cofinite_iff_compl_singleton_mem, ker_def, iInter₂_eq_empty_iff]
  exact forall_congr' fun x => ⟨fun h => ⟨{x}ᶜ, h, by simp⟩,
    fun ⟨s, hs, hx⟩ => mem_of_superset hs (by simpa using hx)⟩

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}
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
obtain ⟨m, hm, hprod⟩ := exists_multiset_of_mem_closure hxy

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