mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun a ↦ [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun x ↦ [b' :: c :: x]) (permutations'Aux a' l) ++
      flatMap (fun a ↦ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
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 • a = a ↔ period m a ∣ n

Tactic:
by
  rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↥s × ↑(QuotientGroup.mk '' t)

Tactic:
apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(QuotientGroup.mk ⁻¹' QuotientGroup.mk '' t)
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
⊢ m < (as.insertIdx n x).length

Tactic:
rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]

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

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

Tactic:
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.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
simpa [Iff.comm] using h a

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
⊢ g ∈ MulAction.stabilizer Rˣ x → g ∈ ⊥

Tactic:
(hg : g.val • x = x)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : ↑g • x = x
⊢ g ∈ ⊥
Module: Mathlib.Algebra.IsPrimePow

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

Tactic:
isPrimePow_nat_iff_bounded_log

Goal state after:
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Cycle α
a b : List α
hab : (IsRotated.setoid α) a b
⊢ (match a with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
rcases a with - | ⟨a, l⟩ <;> rcases b with - | ⟨b, m⟩
      · rfl
      · have := isRotated_nil_iff'.1 hab
        contradiction
      · have := isRotated_nil_iff.1 hab
        contradiction
      · dsimp only
        obtain ⟨n, hn⟩ := hab
        induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

Goal state after:
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
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂

Tactic:
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

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 : (rightRel H) g₁ g₂
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧

Tactic:
replace r := Setoid.symm' _ r

Goal state after:
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 : (rightRel H) g₂ g₁
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a * (a ^ n * c)).primeFactorsList

Tactic:
replicate_succ,

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a :: replicate n a <+~ (a * (a ^ n * c)).primeFactorsList
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n a : ℕ
h : a < n
⊢ (↑a).val = a

Tactic:
val_natCast,

Goal state after:
n a : ℕ
h : a < n
⊢ a % n = a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ (pi Set.univ H).index = ∏ i, (H i).index

Tactic:
simp_rw [index, ← Nat.card_pi]
  refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)
  rw [QuotientGroup.leftRel_pi]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex

Tactic:
rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K

Tactic:
exact isFiniteRelIndex_of_le_right _ le_top

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

Goal state before:
pp: case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = (↑n).val + p * (n / p)

Tactic:
val_natCast,

Goal state after:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = n % p + p * (n / p)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
| #{g | f g = f x}

Tactic:
← map_univ_equiv (Equiv.mulRight y⁻¹),

Goal state after:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
| #({g ∈ map (Equiv.toEmbedding (Equiv.mulRight y⁻¹)) univ | f g = f x})
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑((↑x).val.gcd n) = 1

Tactic:
val_natCast,

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑((x % n).gcd n) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
u : (ZMod 0)ˣ
⊢ (↑u).val.Coprime 0

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Goal state after:
case zero.inl
⊢ (↑1).val.Coprime 0

case zero.inr
⊢ (↑(-1)).val.Coprime 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (↑m).val.Coprime n
⊢ m.Coprime n

Tactic:
val_natCast,

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).Coprime n
⊢ m.Coprime n
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
← erase_insert self_notMem_properDivisors,

Goal state after:
p : ℕ
pp : Prime p
⊢ (insert p p.properDivisors).erase p = {1}
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
by
  refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_
  rcases n with - | n
  · rw [sum_range_zero, zero_mul]
    exact Nat.zero_le _
  rw [mul_comm]
  exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
a✝² a✝¹ a✝ : ℕ
⊢ ¬a✝² = 0 → ((a✝¹ + 1) * (a✝ + 1) = a✝² ↔ -[a✝¹+1] * -[a✝+1] = ↑a✝²)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

Tactic:
simp [ZMod]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ a✝¹ * a✝ = a✝² ∧ ¬a✝² = 0 ∨ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝¹ = 0 ∧ a✝ = 0 ↔ ↑a✝¹ * ↑a✝ = ↑a✝² ∧ ¬a✝² = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝¹ = 0 ↔ ↑a✝¹ * -[a✝+1] = ↑a✝² ∧ ¬a✝² = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝ = 0 ↔ -[a✝¹+1] * ↑a✝ = ↑a✝² ∧ ¬a✝² = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ ¬↑a✝¹ * ↑a✝ = -[a✝²+1]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ a✝¹ * (a✝ + 1) = a✝² + 1 ↔ ↑a✝¹ * -[a✝+1] = -[a✝²+1]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (a✝¹ + 1) * a✝ = a✝² + 1 ↔ -[a✝¹+1] * ↑a✝ = -[a✝²+1]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

Tactic:
simp [divisorsAntidiag]

Goal state after:
case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ ¬-[a✝¹+1] * -[a✝+1] = -[a✝²+1]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
⊢ ∀ (x : ℤ →+ A), x ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ x.ker

Tactic:
intro f
        rw [ker_intCastAddHom]
        constructor
        · rintro hf _ ⟨x, rfl⟩
          simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]
        · intro h
          exact h (AddSubgroup.mem_zmultiples _)

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

Goal state before:
pp: b n : ℕ
⊢ ofDigits b (b.digits n) = n

Tactic:
rcases b with - | b
  · rcases n with - | n
    · rfl
    · simp
  · rcases b with - | b
    · induction n with
      | zero => rfl
      | succ n ih =>
        rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
    · induction n using Nat.strongRecOn with | ind n h => ?_
      cases n
      · rw [digits_zero]
        rfl
      · simp only [digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
rw [← List.dropLast_append_getLast hl]

Goal state after:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ multiplicity a b = multiplicity c d

Tactic:
unfold multiplicity
  rw [h]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
⊢ 0 < multiplicity a b

Tactic:
by
  refine Nat.pos_iff_ne_zero.2 fun h => ?_
  simpa [hdiv] using FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
    (by by_contra! nh; simp [nh] at h) (lt_one_iff.mpr h)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
by rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]
    norm_cast
    exact multiplicity_mul hp hfin

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ False

Tactic:
refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ x ^ (n / a.minFac) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

Tactic:
exact prod_pow_dvd_of_le_factorization inf_le_right

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x)) = x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x)))

Tactic:
simp [zpow_add, zpow_mul, pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
use Fintype.card (G ⧸ zpowers x)

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = orderOf x * card (G ⧸ zpowers x)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
x : G
⊢ orderOf x ∣ Nat.card G

Tactic:
obtain h | h := fintypeOrInfinite G

Goal state after:
case inl
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G

case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
simp only [card_eq_zero_of_infinite, dvd_zero]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
x : k[G]
⊢ of' k G a * x /ᵒᶠ a = x

Tactic:
ext; simp only [of'_apply, coeff_divOf, coeff_single_mul_add, one_mul]

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

Goal state before:
pp: case succ
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
by_cases h : n ∣ N.succ

Goal state after:
case pos
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = 0

Tactic:
Finset.sum_eq_zero

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ 0 = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ f.leadingCoeff ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 hf

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ Irreducible (C a * X + C b)

Tactic:
apply irreducible_of_degree_eq_one_of_isRelPrime_coeff

Goal state after:
case hp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ (C a * X + C b).degree = 1

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime ((C a * X + C b).coeff 0) ((C a * X + C b).coeff 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f * (expand R p) g) = contract p f * g

Tactic:
by
  ext n
  rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
  · simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]
  · intro x hx y hy eq; simpa only [Prod.ext_iff, Nat.mul_right_cancel_iff hp.bot_lt] using eq
  · simp_rw [subset_iff, mem_image, mem_antidiagonal]; rintro _ ⟨x, rfl, rfl⟩; simp_rw [add_mul]
  simp_rw [mem_image, mem_antidiagonal]
  intro ⟨x, y⟩ eq nex
  by_cases h : p ∣ y
  · obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)
    obtain ⟨y, rfl⟩ := h
    refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim
    rw [← eq, mul_comm, mul_add]
  · rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]

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

Goal state before:
pp: case monomial.monomial.succ
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
m : ℕ
⊢ (monomial (m + 1 + n - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n - 1)) (a * (b * ↑n)) =
    (monomial (m + 1 - 1 + n)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n - 1))) (a * (b * ↑n))

Tactic:
cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind

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

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)
p : R[X]
⊢ (⇑derivative)^[k + 1] (map f p) = map f ((⇑derivative)^[k + 1] p)

Tactic:
simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

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
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ leadingCoeff 0 = 0

Tactic:
leadingCoeff_zero

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
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
· apply coeff_eq_zero_of_natDegree_lt
    rw [natDegree_divByMonic p (monic_X_sub_C a), natDegree_X_sub_C]
    exact (Nat.pred_lt hp).trans_le h

Goal state after: