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

Goal state before:
pp: case inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p

Tactic:
refine (hy ?_).elim
    subst hap
    subst ha
    rw [sq, Nat.mul_eq_left (Nat.mul_ne_zero hp.ne_zero hp.ne_zero)] at h
    exact h

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f^[1] x

Tactic:
refine Function.IsPeriodicPt.isFixedPt ?_

Goal state after:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 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 x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
    apply Nat.dvd_of_mul_dvd_mul_right h
    rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]
    apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, iterate_mul]
    exact isPeriodicPt_minimalPeriod _ _

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
⊢ g ^ (j % ↑(period g a)) • a = g ^ j • a

Tactic:
conv_rhs => rw [← Int.emod_add_mul_ediv j (period g a), zpow_add, mul_smul,
    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp [iInf]

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
⊢ x ∈ φ.range → x ∈ map φ ⊤

Tactic:
by rintro ⟨a, ha⟩; exact ⟨a, by simp, ha⟩

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

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup

Tactic:
rw [(permutations_perm_permutations' s).nodup_iff]
  induction hs with
  | nil => simp
  | @cons x l h h' IH =>
    rw [permutations']
    rw [nodup_flatMap]
    constructor
    · intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl
    · refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _

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.reverse.next x ⋯ = l.prev x hx

Tactic:
convert! (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : (orbitRel G α) z a✝
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ∃ g_1, g_1 • ⟨(fun m ↦ m • a✝) g, yh⟩ = ⟨z, zh✝⟩

Tactic:
rcases zh with ⟨h, rfl⟩

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ∃ g_1, g_1 • ⟨(fun m ↦ m • a✝) g, yh⟩ = ⟨(fun m ↦ m • a✝) h, zh⟩
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod

Tactic:
← prod_cons,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ (a :: l₁).prod = a * ((b :: l₂).erase a).prod
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ (a :: l₁).prod = a * ((b :: l₂).erase a).prod

Tactic:
← prod_cons,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ (a :: l₁).prod = (a :: (b :: l₂).erase a).prod
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
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ (comap f H).index = H.index

Tactic:
refine Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)

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

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
K : Subgroup G'
⊢ H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)

Tactic:
← f.map_range,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ H.relIndex (map f K.subtype.range) = H.relIndex (map f K)
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

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast

Tactic:
· apply Int.cast_mul

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast
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'
G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
h : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
rw [← AddSubgroup.finiteIndex_toSubgroup_iff] at h ⊢
  exact H.toSubgroup.finiteIndex_normalCore

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ cons n n.properDivisors ⋯ = n.divisors

Tactic:
rw [cons_eq_insert, insert_self_properDivisors h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors

Tactic:
simp_rw [mem_filter, mem_divisors]

Goal state after:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0

Tactic:
simp [Nat.not_prime_zero]

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

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

Tactic:
right

Goal state after:
case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ 2 * a.val = n✝ + 1
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:
rw [← natCast_val, val_cast_of_lt]

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 < m + 1

case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
right

Goal state after:
case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ n + 1 + [].sum ≤ n + 1

Tactic:
List.sum_nil,

Goal state after:
case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ n + 1 + 0 ≤ n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)

Tactic:
hi,

Goal state after:
case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ emultiplicity a b ≤ ↑n

Tactic:
rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ emultiplicity a b < ↑n

Tactic:
rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a + b

Tactic:
apply dvd_add

Goal state after:
case hk.h₁
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a

case h₂
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
right

Goal state after:
case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ ¬p ∣ n
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:
rwa [card_Ico 1 n.succ] at filter_le_Ico

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x * x ^ (k - 1) * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))

Tactic:
← mul_pow_sub_one (n := p ^ n - k) (by lia)

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x * x ^ (k - 1) * (y * y ^ (p ^ n - k - 1)) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (_root_.frobenius S p) ((algebraMap R S) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s

Tactic:
← (algebraMap R S).map_frobenius

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (algebraMap R S) ((_root_.frobenius R p) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s
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:
rwa [card_Ico 1 n.succ] at filter_le_Ico

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ g ∈ zpowers (g ^ ↑k) ↔ k.gcd (orderOf g) = 1

Tactic:
mem_zpowers_zpow_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ (↑k).gcd ↑(orderOf g) = 1 ↔ k.gcd (orderOf g) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList

Tactic:
count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa),

Goal state after:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ count p a.primeFactorsList + 0 = count p a.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: N n : ℕ
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n

Tactic:
by
  induction N with
  | zero => simp [Finset.filter_false_of_mem]
  | succ N ih =>
    rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * derivative (X ^ p) = eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
derivative_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * (C ↑p * X ^ (p - 1) * derivative X) =
    eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case e'_3.e'_3
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ X = (algEquivAevalXAddC t) (X - C t)

Tactic:
simp [C_eq_algebraMap]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = 1

Tactic:
calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ (aeval x) (map (algebraMap R A) p) = (aeval x) p

Tactic:
by
  rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

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
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
⊢ p %ₘ q = 0

Tactic:
by_contra hpq0

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑q.natDegree + ↑(r - p /ₘ q).natDegree < ↑q.natDegree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)

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

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
      grw [← hsub]
      exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ (⨅ i, l i).HasBasis (fun If ↦ If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun If ↦ ⋂ i, s (↑i) (If.snd i)

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : t ∈ ⨅ i, l i
⊢ ∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t

case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
apply dvd_add

Goal state after:
case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)

case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m.succ] (f ^ n))

Tactic:
Function.iterate_succ_apply,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (derivative (f ^ n)))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (derivative (f ^ n)))

Tactic:
derivative_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (C ↑n * f ^ (n - 1) * derivative f))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ derivative ((X + C c) ^ m) = C ↑m * (X + C c) ^ (m - 1)

Tactic:
derivative_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) * derivative (X + C c) = C ↑m * (X + C c) ^ (m - 1)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)

Tactic:
derivative_pow,

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

Tactic:
by
  rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]

Goal state after: