mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ i (nj j) ∈ M'

Tactic:
rw [← hc, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j' _ ↦ ?_
        let c' : A := ⟨c j j', Subring.subset_closure
          (by simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩])⟩
        rw [show c j j' • mj j' = c' • mj j' from rfl]
        exact smul_mem _ _ (subset_span (by simp))

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
this : ∀ m ∈ p.support, (monomial m) (coeff m p) ∈ I
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I

Tactic:
by
    exact Submodule.sum_mem I this

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ ker (Quotient.mk I) ↔ x✝ ∈ I

Tactic:
ker,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) ⊥ ↔ x✝ ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
⊢ ∃ a, (quotientInfToPiQuotient I) a = g

Tactic:
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      intro j hj
      exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
    rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩
    replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
    refine ⟨e, ?_, ?_⟩
    · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
    · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)

Goal state after:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
key : ∀ (i : ι), ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0
⊢ ∃ a, (quotientInfToPiQuotient I) a = g
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
⊢ Function.Injective fun x ↦ x ^ 2

Tactic:
intro x y h

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x y : R
h : (fun x ↦ x ^ 2) x = (fun x ↦ x ^ 2) y
⊢ x = y
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy

Goal state after:
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p

case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x = p ∧ y = p
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts ys l : List α
⊢ id = fun x ↦ [] ++ x

Tactic:
funext _; rfl

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

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ (y✝ :: x✝ :: l✝).permutations' ~ (x✝ :: y✝ :: l✝).permutations'

Tactic:
| swap =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
this : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
⊢ d ∈ xs → xs.nextOr x d ∈ xs

Tactic:
exact this xs fun _ => id

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

Goal state before:
pp: case cons.left
α : 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
ys : List α
hy : ys ∈ l.permutations'
⊢ (permutations'Aux x ys).Nodup

Tactic:
mem_permutations'

Goal state after:
case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ (permutations'Aux x ys).Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : 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.permutations'
bs : List α
hb : bs ∈ l.permutations'
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' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
⊢ False

Tactic:
mem_permutations'

Goal state after:
case cons.right
α : 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' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
⊢ False
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 ((fun b ↦ b ∈ fixedBy β m) b)

Tactic:
simp only [MulAction.mem_fixedBy]
  infer_instance

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

Tactic:
intro hyp g hg

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

Tactic:
intro hyp g hg

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.prev y hm = l₂.prev y hm'

Tactic:
simpa using isRotated_prev_eq h h₁ _

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k

Tactic:
conv => {lhs; rw [← (pow_one p)]}

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ 1 ≤ p ^ k
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x

Tactic:
rw [mul_smul, ← H, inv_smul_smul]

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
p : ℕ
hp : Prime p
hpn : p ∣ n
⊢ n.primeFactors.Nonempty

Tactic:
exact ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a * b).cast = a.cast * b.cast

Tactic:
apply Int.cast_mul

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'
⊢ Finite ↥f.ker ∧ f.ker.FiniteIndex ↔ Finite ↥f.ker ∧ Finite ↥f.range

Tactic:
← (QuotientGroup.quotientKerEquivRange f).finite_iff,

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 (G ⧸ f.ker)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ val 2 = 2 % n

Tactic:
rw [← Nat.cast_two, val_natCast]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n

Tactic:
rw [val_add_val_of_le h]
  exact eq_tsub_of_add_eq rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Tactic:
refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩

Goal state after:
case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℤ
⊢ ↑n = 1 ↔ Odd n

Tactic:
rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, Int.odd_iff, Int.ModEq]

Goal state after:
n : ℤ
⊢ n % ↑2 = 1 % ↑2 ↔ n % 2 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n ≠ 0 ↔ Odd n

Tactic:
simp [natCast_eq_zero_iff_even]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}

Tactic:
by
  ext
  rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Tactic:
· cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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

Goal state before:
pp: n : ℕ
A : Type u_2
inst✝ : AddGroup A
f : { f // f ↑n = 0 }
⊢ Injective ⇑((lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0

Tactic:
simp only [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff, SetLike.le_def,
    ZMod.intCast_surjective.forall, ZMod.lift_coe, AddMonoidHom.mem_ker, AddSubgroup.mem_bot]

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ (List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i ↦ a * b ^ i) l (List.range l.length)).sum

Tactic:
by
  suffices
    l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
      l.zipWith (fun a i => b * (a * b ^ i)) (List.range l.length)
    by simp [this]
  congr; ext; ring

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n % p ^ i = ofDigits p (List.take i (p.digits n))

Tactic:
by
  convert!
    ofDigits_mod_pow_eq_ofDigits_take i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
and_imp

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ↔ x ^ n = 1

Tactic:
by
  rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
obtain ⟨r, rfl⟩ := hp

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
⊢ ∃ m, x ^ n = x ^ (2 * m)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n.factorization n.minFac ≠ 0

Tactic:
refine mt (factorization_eq_zero_iff _ _).mp ?_
  push Not
  exact ⟨minFac_prime (by lia), minFac_dvd n, Nat.ne_zero_of_lt hn⟩

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ fixedLengthDigits hb l, (i + x.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
rw [Finset.sum_comm]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
rw [ha.multiplicity_eq_iff]
    simp only [pow_one, dvd_refl, reduceAdd, true_and]
    rintro ⟨v, hv⟩
    nth_rw 1 [← mul_one a] at hv
    simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv
    obtain hv | rfl := hv
    · have : IsUnit a := .of_mul_eq_one v hv.symm
      simpa [this] using ha.not_isUnit
    · simpa using ha.ne_zero

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

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

Tactic:
Pi.add_apply

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

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1

Tactic:
by
  rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]

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
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
nth_rewrite 1 [← factorization_pow_self (n := n) hp]

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ (p ^ n).factorization p ≤ ((p ^ n).choose k).factorization p + k.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inr
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
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
· replace hn : n < p ^ i := by
      have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
      calc
        n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
    rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  rw [pow_eq_pow_iff_modEq, h, Nat.modEq_zero_iff]

Goal state after:
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
⊢ emultiplicity p (∏ x ∈ Ico 1 (p * n + 1), x) ≠ ⊤ →
    emultiplicity p (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) =
      emultiplicity p (∏ x ∈ Ico 1 (p * n + 1), x) + emultiplicity p (n + 1) + 1

Tactic:
Finset.emultiplicity_prod hp',

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
⊢ ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤ →
    ∑ x ∈ Ico 1 (p * (n + 1) + 1), emultiplicity p x =
      ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + emultiplicity p (n + 1) + 1
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
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.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hn₀ := eq_or_ne n 0

Goal state after:
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∏ p ∈ n.primeFactors, p ^ n.factorization p ∣ ∏ x ∈ n.primeFactors, x ^ n

Tactic:
refine prod_dvd_prod_of_dvd _ _ fun i hi ↦ pow_dvd_pow i ?_

Goal state after:
n : ℕ
hn : n ≠ 0
i : ℕ
hi : i ∈ n.primeFactors
⊢ n.factorization i ≤ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Finite G
S : Set G
hS1 : S.Nonempty
hS2 : S * S = S
a : G
ha : a ∈ S
⊢ 1 * a⁻¹ ∈ submonoidOfIdempotent S hS1 hS2

Tactic:
← pow_one a,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Finite G
S : Set G
hS1 : S.Nonempty
hS2 : S * S = S
a : G
ha : a ∈ S
⊢ 1 * (a ^ 1)⁻¹ ∈ submonoidOfIdempotent S hS1 hS2
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : ¬q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

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

Goal state before:
pp: case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f

Tactic:
· have := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero

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

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

Tactic:
← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t

Tactic:
· rw [count_cons_of_ne ha, zero_add]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

Tactic:
simp [mul_sum, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

Tactic:
simp [mul_sum, mul_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
⊢ ∑ i, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Tactic:
by
  nontriviality R
  exact
    (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
      (sum_monomial_eq _)

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

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

Tactic:
by
        rw [add_comm, add_assoc]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : X - C a ∣ p
⊢ p.IsRoot a

Tactic:
rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_6
s : ι → Set α
⊢ (⨅ i, 𝓟 (s i)).HasBasis (fun t ↦ t.Finite) fun t ↦ ⋂ i ∈ t, s i

Tactic:
refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩
  simp only [iInf_principal_finset, mem_principal,
    exists_finite_iff_finset, Finset.set_biInter_coe]

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

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

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

Goal state after: