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

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

Tactic:
← zpow_mod_period_smul,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ ((i + ↑(period g a)) % ↑(period g a)) • a = g ^ i • a
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
← zpow_mod_period_smul,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ ((↑(period g a) + i) % ↑(period g a)) • a = g ^ i • a
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
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
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ False

Tactic:
rw [get_permutations'Aux] at hn' hm'

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' : 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
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.next (l.prev 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 + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp [this]

Goal state after:
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
    rw [mem_stabilizer_iff]
    apply subset_antisymm (hyp g hg)
    intro x hx
    use g⁻¹ • x
    constructor
    · apply hyp g⁻¹ (inv_mem hg)
      simp only [Set.smul_mem_smul_set_iff, hx]
    · simp only [smul_inv_smul]

Goal state after:
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₂
x y : α
hxy : x ≍ y
⊢ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂

Tactic:
simpa [eq_of_heq hxy] using h.mem_iff

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

Goal state before:
pp: case cons.cons.succ.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
hn : [a].rotate (d + 1) = b :: m
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])

pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
· simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr.refine_2
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac

Tactic:
grind [Nat.minFac_prime_iff]

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

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
⊢ Prime p

Tactic:
let m := minFac (k + 2)

Goal state after:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
⊢ Prime p
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H

Tactic:
simp [QuotientGroup.eq]

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

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
let m := minFac (k + 2)

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Tactic:
· refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
    rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
    exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
obtain ⟨y, hy⟩ := hf x

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
y : G'
hy : f y = x
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x
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'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (map f H).relIndex (map f (comap f (map f K)))

Tactic:
(gc_map_comap f).l_u_l_eq_l

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (map f H).relIndex (map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ Xor (b * a ∈ H) (b ∈ H) ↔ Xor ((Equiv.inv G) a * (Equiv.inv G) b ∈ H) ((Equiv.inv G) b ∈ H)

Tactic:
simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H * H.index = Nat.card G

Tactic:
card_mul_index

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card G = Nat.card G
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a ∈ H ∨ b ∈ H ↔ (Equiv.inv G) a * (Equiv.inv G) b ∈ H ∨ (Equiv.inv G) b ∈ H

Tactic:
simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬H.relIndex K = 1

Tactic:
relIndex_eq_one

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝² : Ring R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Module (ZMod n) R
r : ZMod n
x : R
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
obtain _ | n := n
    · obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _
      simp [ZMod, Int.cast_comm]
    · obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
      simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ⇑(Equiv.prodComm ℕ ℕ) '' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Tactic:
Equiv.coe_prodComm,

Goal state after:
n : ℕ
⊢ Prod.swap '' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Tactic:
rintro (hn | hx')

Goal state after:
case refine_2.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

case refine_2.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod 0
y : ZMod 1
⊢ to_fun (inv_fun (x, y)) = (x, y)

Tactic:
fin_cases y

Goal state after:
case inl.right.«0»
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod 0
⊢ to_fun (inv_fun (x, (fun i ↦ i) ⟨0, ⋯⟩)) = (x, (fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k

pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y

Tactic:
· simpa using congr_arg ((↑) : ℕ → ZMod m) ha

Goal state after:
case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.w₂
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
h : L ≠ []
w₂ : L.getLast h ≠ 0
⊢ L.getLast h ≠ 0

Tactic:
convert! w₂

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

Goal state before:
pp: case zero
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n

Tactic:
rcases n with - | n
    · rfl
    · simp

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

Goal state before:
pp: case inr.refine_1.inl
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

Tactic:
exact digits_lt_base hb h

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

Goal state before:
pp: case inr.refine_1.inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b

Tactic:
exact digits_lt_base hb h

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

Goal state before:
pp: case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
    hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ tl₂)

Tactic:
rw [← ih₁ h.symm, mul_add]

Goal state after:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m n : ℕ
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

Goal state after:
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 (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)

Tactic:
← List.drop_one,

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 1 (List.drop i digits)) = ofDigits p (List.drop (i + 1) digits)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Tactic:
intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : IsOfFinOrder (a ^ n)
hn : n ≠ 0
⊢ IsOfFinOrder a

Tactic:
by
  rw [isOfFinOrder_iff_pow_eq_one] at *
  rcases h with ⟨m, hm, ha⟩
  exact ⟨n * m, mul_pos hn.bot_lt hm, by rwa [pow_mul]⟩

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

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
rw [← Nat.lt_add_one_iff, lt_iff_not_ge,
      le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
    intro h
    have := h.count_le p
    simp at this

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

pp: case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Tactic:
· simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
    contrapose hm
    simp only [not_and_or, not_not] at hm ⊢
    exact hm.or_of_add

Goal state after:
case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
· exact fun x hx ↦ lt_of_mem_digitsAppend hb l x hx

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a ∈ Finset.range b, L ∈ consFixedLengthDigits hb l a

Tactic:
Finset.mem_range,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, L ∈ consFixedLengthDigits hb l a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_left_comm, pow_add]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p

Tactic:
simp_all [mul_comm, mul_left_comm, pow_add]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 ↦ x * x_1) 1 / (minimalPeriod (fun x_1 ↦ x * x_1) 1).gcd n

Tactic:
← minimalPeriod_iterate_eq_div_gcd h,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x * x_1)^[n] 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1

Tactic:
by
  rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
  · rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
  · rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ x ^ m * (x ^ n)⁻¹ = 1 ↔ m ≡ n [ZMOD ↑(orderOf x)]

Tactic:
← zpow_sub,

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ x ^ (m - n) = 1 ↔ m ≡ n [ZMOD ↑(orderOf x)]
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)

Tactic:
· ext n
    simp [coeff_X_pow]

Goal state after:
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✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ card ↑(S ^ card G) = card ↑(S ^ (card G + card G))

Tactic:
Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
    constructor
    · intro h
      rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
      rw [Nat.dvd_iff_mod_eq_zero]
      apply hR _ (Nat.mod_lt _ _) h
      rw [← hn, Fintype.card_pos_iff]
      exact ⟨0⟩
    · rintro ⟨n, rfl⟩
      rw [Nat.cast_mul, H, zero_mul]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.natDegree = deg

Tactic:
subst coeff_eq deg_eq_deg coeff_eq_deg

Goal state after:
R : Type u_1
inst✝ : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hgf

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
constructor <;> intro h
  · induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
  · rcases h with ⟨t, hts, tfin, h⟩
    exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
by rw [eq_C_of_natDegree_eq_zero hp, derivative_C]

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

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
i : ℕ
⊢ s ↑(x i) ∈ f

Tactic:
cases i

Goal state after:
case zero
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
⊢ s ↑(x 0) ∈ f

case succ
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
n✝ : ℕ
⊢ s ↑(x (n✝ + 1)) ∈ f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p

Tactic:
simp [add_mul]

Goal state after: