mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
h : i ≠ j
⊢ (IsCoprime on f) i j

Tactic:
fin_cases i

Goal state after:
case «0»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r

Tactic:
induction L with

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (map length L).sum = n * L.length

Tactic:
induction L with

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
hmn' : n < m
⊢ False

Tactic:
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * ((is.permutationsAux []).length + 1) + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + 1 + is.length)!

Tactic:
IH2,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! = (ts.length + 1 + is.length)!
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ l ~ [a, b] ↔ l = [a, b] ∨ l = [b, a]

Tactic:
have : [a, b].permutations = [[a, b], [b, a]] := by cbv

Goal state after:
α : Type u_1
a b : α
l : List α
this : [a, b].permutations = [[a, b], [b, a]]
⊢ l ~ [a, b] ↔ l = [a, b] ∨ l = [b, a]
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
S : Set (StarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ some (l.nextOr a d) = l[idxOf a l + 1]?

Tactic:
by
  match l with
  | nil => simp at ha
  | [head] => simp at ha
  | x :: y :: tail =>
    rw [getElem?_cons_succ, nextOr]
    split_ifs with hx
    · grind
    rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
    grind

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
⊢ ∃ a, a ∈ L ∧ p ∣ a

Tactic:
induction L with

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ˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
⊢ p ∈ L

Tactic:
obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

Tactic:
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl

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
⊢ ¬K ≤ H

Tactic:
exact h.not_ge

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n.succ | d ∣ n} = n.divisors

Tactic:
by
  ext
  simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

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

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

Tactic:
rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases y
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases x
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
by
  rw [neg_eq_iff_add_eq_zero, ← two_mul]
  cases n
  · simp
  conv_lhs =>
    rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]
  constructor
  · rintro ⟨m, he⟩
    rcases m with - | m
    · rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)
    cases m
    · right
      rwa [show 0 + 1 = 1 from rfl, mul_one] at he
    refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
    rw [he, mul_comm]
    apply Nat.mul_le_mul_left
    simp
  · rintro (rfl | h)
    · rw [val_zero, mul_zero]
      apply dvd_zero
    · rw [h]

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

Goal state before:
pp: n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)

Tactic:
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L

Tactic:
induction L with

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

Goal state before:
pp: case inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
· rw [mul_zero, zero_add]

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
induction L with

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

Goal state before:
pp: b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ l ∈ L, l < b
w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0
⊢ b.digits (ofDigits b L) = L

Tactic:
induction L with

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

Goal state before:
pp: L : List ℕ
⊢ ofDigits 1 L = L.sum

Tactic:
induction L with

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

Goal state before:
pp: L : List ℕ
⊢ ofDigits 1 L = L.sum

Tactic:
induction L with
  | nil => rfl
  | cons _ _ ih => simp [ofDigits, List.sum_cons, ih]

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

Goal state before:
pp: p n : ℕ
⊢ p ^ padicValNat p n * n.divMaxPow p = n

Tactic:
rw [Nat.mul_comm, divMaxPow_mul_pow_padicValNat]

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

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum

Tactic:
induction L with

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

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

Tactic:
rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h

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

Goal state before:
pp: b : ℕ
hb : 1 < b
L1 L2 : List ℕ
len : L1.length = L2.length
w1 : ∀ l ∈ L1, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b L1 = ofDigits b L2
⊢ L1 = L2

Tactic:
induction L1 generalizing L2 with
  | nil =>
    simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  | cons D L ih => ?_
  obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm
  simp only [List.length_cons, add_left_inj] at len
  simp only [ofDigits_cons] at h
  have eqd : D = d := by
    have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
    simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H
  simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h
  have := ih len (fun a ha ↦ w1 a <| List.mem_cons_of_mem D ha)
    (fun a ha ↦ w2 a <| List.mem_cons_of_mem d ha) h
  rw [eqd, this]

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

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ d < b + 2

pp: case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits (n + 1)
⊢ d < b + 2

Tactic:
· rw [digits_zero] at hd
    cases hd

Goal state after:
case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits (n + 1)
⊢ d < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L

Tactic:
induction L with

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

Goal state before:
pp: case inl
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
induction L with

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

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
⊢ k ∣ ofDigits a L - ofDigits b L

Tactic:
induction L with

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

Goal state before:
pp: b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]

Tactic:
induction L with

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

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

Tactic:
induction L with

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

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

Tactic:
induction f with

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

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
induction f with

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬IsOfFinOrder x

Tactic:
by
  simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
  intro n hn_pos hnx
  rw [← pow_zero x] at hnx
  rw [h hnx] at hn_pos
  exact irrefl 0 hn_pos

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
orderOf_eq_zero_iff,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ ¬IsOfFinOrder x ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ orderOf 0 = 0

Tactic:
orderOf_eq_zero_iff,

Goal state after:
M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ ¬IsOfFinOrder 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b ^ (l - 1).succ

Tactic:
Nat.sub_one,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b ^ l.pred.succ
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

pp: case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
· rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]

Goal state after:
case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
by
        rw [factorization_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), add_left_inj]
        apply factorization_eq_card_pow_dvd_of_lt hp (zero_lt_succ n)
          (lt_pow_of_log_lt hp.one_lt hb)

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ False

Tactic:
have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d * d).factorization = n.factorization

Tactic:
Nat.div_mul_cancel h

Goal state after:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ n.factorization = n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)

Tactic:
apply minimalPeriod_eq_prime_pow

Goal state after:
case hk
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ ¬IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ n) 1

case hk1
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ (n + 1)) 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom

Tactic:
apply prod_pow_factorization_choose

Goal state after:
n : ℕ
⊢ n ≤ 2 * n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ emultiplicity p (p * n)! ≠ ⊤ → emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
simp_rw [← prod_Ico_id_eq_factorial, Finset.emultiplicity_prod hp', ← sum_Ico_consecutive _ h1 h3,
    add_assoc]

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤ →
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x =
      ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}

Tactic:
· congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

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
x : k[G]
g : G
⊢ x * of' k G g %ᵒᶠ g = 0

Tactic:
by
  ext g'
  simp only [of'_apply, coeff_zero, Finsupp.zero_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [coeff_modOf_self_add]
  · rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_mul_single_of_forall_add_ne]
    simpa [eq_comm, add_comm] using h

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ((p + q).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) =
    (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
rw [sum_add_index] <;>
      simp only [add_mul, forall_const, map_add, zero_mul, map_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree) + q.degree

Tactic:
degree_eq_natDegree hq0,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree) + ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ 1 + derivative (C c) = 1

Tactic:
derivative_C,

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
⊢ 1 + 0 = 1
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
⊢ f.coeff (p * x, y).1 * ((expand R p) g).coeff (p * x, y).2 = 0

Tactic:
obtain ⟨y, rfl⟩ := h

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ f.coeff (p * x, p * y).1 * ((expand R p) g).coeff (p * x, p * y).2 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n

Tactic:
Nat.div_mul_cancel h

Goal state after:
case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff n = f.coeff n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n

Tactic:
rw [Nat.div_mul_cancel h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ i ∈ range n.succ, (n.choose i + n.choose i.succ) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
Nat.succ_sub_succ,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ x ∈ range n.succ, (n.choose x + n.choose x.succ) • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)

Tactic:
refine sum_congr rfl fun k hk => ?_

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k ∈ range n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
add_comm (q * _),

Goal state after:
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + q * (p₁ /ₘ q) + p₂ = p₁ + p₂