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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain (fun a b ↦ r (f^[a] x) (f^[b] x)) ↑(List.range (minimalPeriod f x - succ 0 + succ 0)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)

Tactic:
Cycle.chain_range_succ

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) ↔
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
clear p
    subst e
    rcases append_of_mem (p'.symm.subset mem_cons_self) with ⟨l₁, l₂, e⟩
    subst is'
    have p := (perm_middle.symm.trans p').cons_inv
    rcases l₂ with - | ⟨a, l₂'⟩
    · exact Or.inl ⟨l₁, by simpa using p⟩
    · exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ [a, b].permutations = [[a, b], [b, a]]

Tactic:
cbv

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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ m ^ minimalPeriod (fun x ↦ m • x) a • a = a

Tactic:
← smul_iterate_apply,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ (fun x ↦ m • x)^[minimalPeriod (fun x ↦ m • x) a] a = a
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
n : ℕ
⊢ IsPeriodicPt (fun x ↦ m • x) n a ↔ m ^ n • a = a

Tactic:
← smul_iterate_apply,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
n : ℕ
⊢ IsPeriodicPt (fun x ↦ m • x) n a ↔ (fun x ↦ m • x)^[n] a = a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : 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
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
nextOr_cons_of_ne _ _ _ _ hx

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = (z :: head✝ :: tail✝).prev x ⋯

Tactic:
rw [prev, dif_neg hy, if_neg hz]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
· rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)

Goal state after:
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✝ y : α
yh✝ : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
yh : (orbitRel G α) y a✝
z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : (orbitRel G α) z a✝
⊢ ∃ g, g • ⟨y, yh✝⟩ = ⟨z, zh✝⟩

Tactic:
rcases yh with ⟨g, rfl⟩

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

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

Tactic:
have := isRotated_nil_iff'.1 hab

Goal state after:
case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
this : [] = b :: m
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Goal state after:
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 * (a ^ n * c) = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
mul_eq_zero,

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)
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x - y).cast = (↑(x.cast - y.cast)).cast

Tactic:
Int.cast_sub,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = (↑x.cast - ↑y.cast).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1

Tactic:
Int.cast_sub,

Goal state after:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑k - ↑1 = ↑k - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z

Tactic:
· rintro ⟨k, rfl⟩
    rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
split_ifs at ih ⊢ with h

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0
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')
    · exact hn.geom_sum_pos
    · exact geom_sum_pos' hx' hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + (0 + ∑ x ∈ s, x)

Tactic:
← add_assoc,

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + 0 + ∑ x ∈ s, x
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n → 0 = x + 1 ∨ 0 < x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
or_comm

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n → 0 < x + 1 ∨ 0 = x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Goal state after:
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:
by
  rw [div_le_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r
  exact mod_cast r.factorial_pos

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

Goal state before:
pp: case neg
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
cases n with

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

Goal state before:
pp: case h
n : ℕ
⊢ (n + 1 + (n + 1)).choose (n + 1) = 2 * (n + 1 + n).choose n

Tactic:
← add_assoc,

Goal state after:
case h
n : ℕ
⊢ (n + 1 + n + 1).choose (n + 1) = 2 * (n + 1 + n).choose n
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
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ l ∈ L, l < b

Tactic:
intro l m

Goal state after:
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
w₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l < b
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
h : ¬p ∣ n
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
cases n with

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

Goal state before:
pp: p n : ℕ
⊢ (p.maxPowDvdDiv n).snd * p ^ (p.maxPowDvdDiv n).fst = n

Tactic:
fun_cases maxPowDvdDiv with

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

Goal state before:
pp: p : ℕ
hp : 1 < p
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k) = (k, 1)

Tactic:
simpa using maxPowDvdDiv_base_pow_mul hp Nat.one_ne_zero k

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

Goal state before:
pp: case cons
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 = (d + b' * ofDigits b' L) % k

Tactic:
conv_rhs => rw [Nat.add_mod, Nat.mul_mod]

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

Goal state before:
pp: case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
← Nat.ofDigits_digits b (n + 1)

Goal state after:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ multiplicity p n = n.factorization p

Tactic:
simp [factorization, pp, padicValNat_def' pp.ne_one hn]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k : ℕ
x✝ : FiniteMultiplicity p a
⊢ ¬p ^ (0 + 1) ∣ a ^ 0

Tactic:
by simp [mt isUnit_iff_dvd_one.2 hp.2.1]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
exact ⟨hdiv, hsucc⟩

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.factorization p = 1

Tactic:
by simp [hp]

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

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) + #({i ∈ Ico 1 (n + 1) | p ^ i ∣ k}) ≤ n

Tactic:
← card_union_of_disjoint hdisj,

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i} ∪ {i ∈ Ico 1 n.succ | p ^ i ∣ k}) ≤ n
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
by
  rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

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

Goal state before:
pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization

Tactic:
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb

Goal state after:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
heb' : e.factorization ≤ b.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 = 0
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Goal state after:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
⊢ orderOf x ≤ Nat.card G

Tactic:
obtain ⟨⟩ := nonempty_fintype G

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ Nat.card G
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) + #({i ∈ Ico 1 n.succ | p ^ i ∣ k}) ≤ n

Tactic:
← card_union_of_disjoint hdisj,

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i} ∪ {i ∈ Ico 1 n.succ | p ^ i ∣ k}) ≤ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b

Tactic:
rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]
    apply lt_of_le_of_lt (le_of_dvd (Nat.zero_lt_of_ne_zero hn) h1) hb

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

Goal state before:
pp: n : ℕ
p1 : ↥n.primeFactors
⊢ ∀ ⦃j : ↥n.primeFactors⦄, p1 ≠ j → Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 j

Tactic:
p2

Goal state after:
n : ℕ
p1 p2 : ↥n.primeFactors
⊢ p1 ≠ p2 → Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 p2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := ⋯
c : ℕ := ⋯
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ (fun a ↦ a ^ n) b = (fun a ↦ a ^ n) (c ^ m)

Tactic:
simp [← h, ha, Nat.pow_right_comm]

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

Goal state before:
pp: case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (C (q.coeff 0) + p)

Tactic:
exact h_C_add hp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ (expand R p) f = f.sum fun e a ↦ C a * (X ^ p) ^ e

Tactic:
simp [expand, eval₂_eq_sum]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ (expand R 1) f = (⇑(expand R p))^[Nat.zero] f

Tactic:
expand_one,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
⊢ f = (⇑(expand R p))^[Nat.zero] f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = f.coeff (n / p)

pp: case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
Nat.mul_div_cancel' h,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (if n = n then f.coeff (n / p) else 0) = f.coeff (n / p)

case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ b ∈ f.support, b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + (1 + n)) ∣ p * (X - C a) ^ n

Tactic:
← add_assoc,

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1 + n) ∣ p * (X - C a) ^ n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inl
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 + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [h']

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
⊢ (expand R p) (contract p f) = f

Tactic:
obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›

Goal state after:
case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

Tactic:
expand_one,

Goal state after:
case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ contract 1 f = f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

pp: case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f

Tactic:
· rw [expand_one, contract_one]

Goal state after:
case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by
        unfold divByMonic divModByMonicAux
        simp [dif_pos hq, h, degree_zero, bot_le]

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

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

Goal state before:
pp: case inr
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 : ¬g.IsRoot (r ^ p ^ n)
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
← eval_X (x := r),

Goal state after:
case inr
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 : ¬g.IsRoot (eval r X ^ p ^ n)
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
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 : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have hgf := hfg

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
    eq_of_sub_eq_zero
      (by
        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
        simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ f /ₘ g = q ∧ f %ₘ g = r