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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [nextOr, nextOr, IH]
    simpa [h] using x_mem

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Tactic:
by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

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

Goal state before:
pp: case h₁
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬minimalPeriod f x ∣ p ^ k

Tactic:
← isPeriodicPt_iff_minimalPeriod_dvd

Goal state after:
case h₁
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬IsPeriodicPt f (p ^ k) x
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case h₂
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)

Tactic:
← isPeriodicPt_iff_minimalPeriod_dvd

Goal state after:
case h₂
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ IsPeriodicPt f (p ^ (k + 1)) x
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
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup

Tactic:
nodup_flatMap

Goal state after:
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_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
⊢ l[i + idxOf a l]? = some [a, l.nextOr a d][i]

Tactic:
· have ⟨_, _⟩ := l.dropLast_prefix
    grind

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
⊢ l[i + idxOf a l]? = some [a, l.nextOr a d][i]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : i = 1
⊢ l[i + (idxOf a l - 1)]? = some [l.prev a ha, a][i]

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : ¬i = 1
⊢ l[i + (idxOf a l - 1)]? = some [l.prev a ha, a][i]

Tactic:
· subst hi₁
    grind

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : ¬i = 1
⊢ l[i + (idxOf a l - 1)]? = some [l.prev a ha, a][i]
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 : α
g h : G
⊢ (h * g⁻¹) • ⟨(fun m ↦ m • a) g, ⋯⟩ = ⟨(fun m ↦ m • a) h, ⋯⟩

Tactic:
ext1

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 h : G
⊢ ↑((h * g⁻¹) • ⟨(fun m ↦ m • a) g, ⋯⟩) = ↑⟨(fun m ↦ m • a) h, ⋯⟩
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Tactic:
MulAction.mem_stabilizer_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ swap a b • S = S ↔ (a ∈ S ↔ b ∈ S)
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
by
  cases n
  · rw [Nat.mod_zero]
    exact Int.natAbs_natCast a
  · apply Fin.val_natCast

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

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (finCongr h).toFun (a + b) = (finCongr h).toFun a + (finCongr h).toFun b

Tactic:
dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K

Tactic:
convert! pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn
  simp [pow_mem ha, mem_subgroupOf]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑a = ↑0 ↔ ↑b ∣ a

Tactic:
ZMod.intCast_eq_intCast_iff,

Goal state after:
a : ℤ
b : ℕ
⊢ a ≡ 0 [ZMOD ↑b] ↔ ↑b ∣ a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℤ
c : ℕ
⊢ ↑a = ↑b ↔ ↑c ∣ b - a

Tactic:
ZMod.intCast_eq_intCast_iff,

Goal state after:
a b : ℤ
c : ℕ
⊢ a ≡ b [ZMOD ↑c] ↔ ↑c ∣ b - a
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝¹ : Semiring R
inst✝ : Fintype M'
⊢ #R[M'] = lift.{v, u} #R ^ card M'

Tactic:
simp [coeffEquiv.cardinal_eq]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (b : ℕ × ℕ),
        (have y := n / a;
            if a * y = n then some (a, y) else none) =
            some b →
          ∀ (b' : ℕ × ℕ),
            (have y := n / a';
                if a' * y = n then some (a', y) else none) =
                some b' →
              b.2 > b'.2
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
ZMod.intCast_eq_intCast_iff,

Goal state after:
n : ℤ
⊢ n ≡ 1 [ZMOD ↑2] ↔ Odd n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
  apply_fun (a * ·) at H
  rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

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

Goal state before:
pp: case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun

pp: case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
· intro x; rfl

Goal state after:
case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun

pp: case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
· intro x; rfl

Goal state after:
case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ r ! * n.choose r ≤ n ^ r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ k ! * n.choose k < n ^ k

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ n.choose k < 2 ^ n

Tactic:
refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)
  rw [← Nat.sub_add_cancel p]
  exact choose_succ_le_two_pow (n - 1) k

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

Goal state before:
pp: case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0

pp: case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n

Tactic:
· cases k <;> simp

Goal state after:
case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ 2 ∣ n.centralBinom

Tactic:
← Nat.succ_pred_eq_of_pos h

Goal state after:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']

Goal state after:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ (fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p) = p

Tactic:
ext1

Goal state after:
case fst
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).1 = p.1

case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)

Tactic:
by
  apply maxPowDvdDiv_of_pow_mul_eq
  · exact Nat.mul_ne_zero (Nat.ne_of_gt <| Nat.pow_pos <| Nat.zero_lt_of_lt hp) hn
  · rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]
  · exact not_dvd_divMaxPow hp hn

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

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

Tactic:
have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]

Goal state after:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b
⊢ D = d
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b * ofDigits b L) % ↑k

Tactic:
rw [Int.add_emod, Int.mul_emod, h, ih]

Goal state after:
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
by cases h <;> simp [*]

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

Goal state before:
pp: case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ n.factorization + k • n.factorization = (k + 1) • n.factorization

Tactic:
add_smul,

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ n.factorization + k • n.factorization = k • n.factorization + 1 • n.factorization
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
hb.multiplicity_add_of_gt hab,

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b = min (multiplicity p a) (multiplicity p b)
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
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
tsub_add_cancel_of_le (succ_le_of_lt hn0)

Goal state after:
α : 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
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ n * y
⊢ p * x * p = p ^ (n + 1) * y * p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

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

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ i ∈ Ico 1 (multiplicity m n + 1) ↔ i ∈ {i ∈ Ico 1 b | m ^ i ∣ n}

Tactic:
by
            simp only [mem_Ico, Nat.lt_succ_iff,
              fin.pow_dvd_iff_le_multiplicity, mem_filter,
              and_assoc, and_congr_right_iff, iff_and_self]
            intro hi h
            rw [← fin.pow_dvd_iff_le_multiplicity] at h
            rcases m with - | m
            · rw [zero_pow, zero_dvd_iff] at h
              exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]
            refine LE.le.trans_lt ?_ hb
            exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
                (le_of_dvd hn h)

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p n ! + emultiplicity p (n + 1) = ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1}))

Tactic:
by
        rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization

Tactic:
ext1

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ (a.factorization + b.factorization) a✝ = (a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization) a✝
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:
Int.gcd_dvd_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x y, ↑1 = k * x + ↑(orderOf g) * y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivZPowers_symm_apply]

Goal state after:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (∃ m, n ∣ k ^ m) ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
refine ⟨fun ⟨m, h⟩ ↦ ?_, fun h ↦ ⟨n, dvd_pow_self_iff hn hk |>.mpr h⟩⟩

Goal state after:
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
⊢ n.primeFactors ⊆ k.primeFactors
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
by
        have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
· exact natDegree_pow_le_of_le m ‹_›

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (expand R p) X ^ q = r • X ^ (q * p)

Tactic:
expand_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (X ^ p) ^ q = r • X ^ (q * p)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * (expand R p) ((expand R q) X) ^ (n + 1) = C r * (expand R (p * q)) X ^ (n + 1)

Tactic:
expand_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * (expand R p) (X ^ q) ^ (n + 1) = C r * (X ^ (p * q)) ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * ((expand R p) X ^ q) ^ (n + 1) = C r * (X ^ (p * q)) ^ (n + 1)

Tactic:
expand_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * ((X ^ p) ^ q) ^ (n + 1) = C r * (X ^ (p * q)) ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * (expand R 1) X ^ (n + 1) = C r * X ^ (n + 1)

Tactic:
expand_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * (X ^ 1) ^ (n + 1) = C r * X ^ (n + 1)
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.natDegree * p) ≤ ((expand R p) f).degree

Tactic:
· refine le_degree_of_ne_zero ?_
    rw [coeff_expand_mul hp, ← leadingCoeff]
    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✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = 0 + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
map_one,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (1 * (X - C a) ^ n) = 0 + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivative (X ^ 2) = C 2 * X

Tactic:
rw [derivative_X_pow, Nat.cast_two, pow_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ -C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
    rw [← C_1]
    congr
    exact h.val_inv_mul

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r
    (((expand R (p ^ n)) X - (expand R (p ^ n)) (C (r ^ p ^ n))) ^ rootMultiplicity (r ^ p ^ n) f *
      (expand R (p ^ n)) g)

Tactic:
expand_X,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r
    ((X ^ p ^ n - (expand R (p ^ n)) (C (r ^ p ^ n))) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)
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 : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = (algebraMap A B) (eval₂ (algebraMap R A) x p)

Tactic:
hom_eval₂,

Goal state after:
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 : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = eval₂ ((algebraMap A B).comp (algebraMap R A)) ((algebraMap A B) x) p