mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.add
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x y✝ : ↥N
y : x ∈ span (↥A) ({n} ∪ Set.range nj)
hy✝ : y✝ ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A f) x ∈ M'
hy : (↑↥A f) y✝ ∈ M'
⊢ (↑↥A f) (x + y✝) ∈ M'

Tactic:
rw [map_add]

Goal state after:
case refine_2.add
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x y✝ : ↥N
y : x ∈ span (↥A) ({n} ∪ Set.range nj)
hy✝ : y✝ ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A f) x ∈ M'
hy : (↑↥A f) y✝ ∈ M'
⊢ (↑↥A f) x + (↑↥A f) y✝ ∈ M'
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n

Tactic:
← Int.ofNat_inj

Goal state after:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ c + b * n [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
modEq_add_mul_modulus_iff

Goal state after:
n a b c : ℤ
⊢ a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔ ¬m = n

Tactic:
have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations

Goal state after:
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  _root_.Disjoint ↑m.toList.permutations ↑n.toList.permutations ↔ m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔ ¬m = n
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n

pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
· intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd

Tactic:
by
  induction ts with | nil => rfl | cons a ts ih => ?_
  simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
    cons.injEq, true_and]
  simp +singlePass only [← permutationsAux2_append]
  simp [map_permutationsAux2]

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

Goal state before:
pp: α : Type u_1
is : List α
⊢ [].permutationsAux is = []

Tactic:
rw [permutationsAux, permutationsAux.rec]

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ (t :: ts).permutationsAux is =
    foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations

Tactic:
rw [permutationsAux, permutationsAux.rec]

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x ↦ [])
        (fun t ts is IH1 IH2 ↦ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x ↦ [])
          (fun t ts is IH1 IH2 ↦ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) is []) =
    foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
by
  rw [add_comm] at hn
  exact hn.left_of_add hm

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit_chain r]
  refine ⟨fun H n => ?_, fun H n _ => H n⟩
  rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]
  exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯

Tactic:
prev,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (if hx : x = y then (z :: l).getLast ⋯ else if x = z then y else (z :: l).prev x ⋯) = (z :: l).getLast ⋯
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 = y

Tactic:
prev,

Goal state after:
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✝
⊢ (if hx : x = y then (z :: head✝ :: tail✝).getLast ⋯ else if x = z then y else (z :: head✝ :: tail✝).prev x ⋯) = y
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:
prev,

Goal state after:
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✝
⊢ (if hx : x = y then (z :: head✝ :: tail✝).getLast ⋯ else if x = z then y else (z :: head✝ :: tail✝).prev x ⋯) =
    (z :: head✝ :: tail✝).prev x ⋯
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:
prev,

Goal state after:
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
⊢ (if hx : x = hd then (hd' :: tl).getLast ⋯ else if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ [l.prev a ha, a] <:+: l

Tactic:
have := cons_head_tail (ne_nil_of_mem ha) ▸ idxOf_cons_ne _ <| Ne.symm ha₀
  refine infix_iff_getElem?.mpr ⟨l.idxOf a - 1, by grind, fun i hi ↦ ?_⟩
  by_cases hi₁ : i = 1
  · subst hi₁
    grind
  grind [prev_eq_getElem?_idxOf_pred_of_ne_head]

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

Goal state before:
pp: case cons.right.inr.inr
α : 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
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
⊢ x ∈ as

Tactic:
← hx,

Goal state after:
case cons.right.inr.inr
α : 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
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
⊢ (as.insertIdx n x)[m] ∈ as
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose = ⋯.choose * ↑g⁻¹

Tactic:
refine IsCancelSMul.right_cancel _ _ (g • y₂) ?_

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose • g • y₂ = (⋯.choose * ↑g⁻¹) • g • y₂
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ZMod 0
⊢ IsUnit n ↔ n.val = 1

Tactic:
by
  simp only [val]
  rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

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

Goal state before:
pp: n : ℕ
⊢ CharP (ZMod n) n

Tactic:
exact ZMod.charP n

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
obtain ⟨a, b⟩ := x

Goal state after:
n a b : ℕ
⊢ (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
m₁ : Module (ZMod n) M
inst✝ : Module R M
⊢ IsScalarTower (ZMod n) R M

Tactic:
by
  let := ZMod.algebraOfModule n R
  let m₂ := Module.compHom M (algebraMap (ZMod n) R)
  obtain rfl : m₁ = m₂ := Subsingleton.elim _ _
  exact ⟨fun x y z ↦ by rw [Algebra.smul_def, mul_smul]; rfl⟩

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)

Tactic:
by rw [← mul_add, add_tsub_cancel_of_le (by lia)]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ (n * (↑n)⁻¹.val) = a

Tactic:
← pow_mod_natCard,

Goal state after:
α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ (n * (↑n)⁻¹.val % Nat.card α) = a
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:
by
    ext1
    · simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]
    · simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

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

Goal state before:
pp: case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q

Tactic:
List.getLast_cons

Goal state after:
case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (b.digits (m / b)).getLast ?neg✝ = (b.digits (m / b)).getLast q

case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ b.digits (m / b) ≠ []
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
k : ℕ
⊢ (p ^ k).divMaxPow p = 1

Tactic:
simpa using divMaxPow_base_pow_mul hp 1 k

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

Goal state before:
pp: case inr.refine_2
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
by_cases h : digits b m = []
    · simp only [h, List.append_nil] at h_append ⊢
      exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append
    · exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

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

Goal state before:
pp: b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_
  intro d hd
  rcases n with - | n
  · rw [digits_zero] at hd
    cases hd
  -- base b+2 expansion of 0 has no digits
  rw [digits_add_two_add_one] at hd
  cases hd
  · exact n.succ.mod_lt (by linarith)
  · apply IH ((n + 1) / (b + 2))
    · apply Nat.div_lt_self <;> lia
    · assumption

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

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

Tactic:
by
  nth_rewrite 2 [← (setInvOn_digitsAppend_ofDigits hb l).1 hL]
  rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 ↦ x * x_1 then Nat.find h else 0) = n ↔
    IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ (p * i + r).factorization p = 0

Tactic:
by
  refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩
  rw [factorization_eq_zero_iff] at h
  contrapose! h
  refine ⟨pp, ?_, ?_⟩
  · rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]
  · contrapose hr0
    exact (add_eq_zero.1 hr0).2

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
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
by rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

Goal state after:
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).factorization + d.factorization = n.factorization - d.factorization + d.factorization

Tactic:
tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h,

Goal state after:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

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

Goal state before:
pp: case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0

pp: case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ (n.choose k).factorization p = 0

Tactic:
· exact factorization_eq_zero_of_not_prime (choose n k) hp

Goal state after:
case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
← hp.emultiplicity_mul,

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * (k ! * n !)) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
exact emultiplicity_le_emultiplicity_choose_add hp _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ (∏ p ∈ n.primeFactors, p) ^ n

Tactic:
by
  nth_rw 1 [← Finset.prod_pow, prod_primeFactors_pow_factorization hn]
  refine prod_dvd_prod_of_dvd _ _ fun i hi ↦ pow_dvd_pow i ?_
  grw [n.factorization_def <| prime_of_mem_primeFactors hi, padicValNat_le_self]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
by rintro ⟨_ | _⟩ <;> simp [coeff_C, coeff_mul_X]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ CharP R (p ^ n)

Tactic:
obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hc : CharP R (p ^ i)
hn : card R = p ^ i
hR : ∀ i_1 ≤ i, ↑p ^ i_1 = 0 → i_1 = i
hi : i ≤ i
hcpn : p ^ i ∣ p ^ i
⊢ CharP R (p ^ i)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ (x✝¹ * x✝).IsRoot r → x✝¹.IsRoot r ∨ x✝.IsRoot r

Tactic:
IsRoot.def,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r (x✝¹ * x✝) = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 0 = f.coeff (n * p)

Tactic:
apply (coeff_eq_zero_of_natDegree_lt _).symm

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < n * p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
by
  rcases eq_or_ne (derivative p) 0 with hp' | hp'
  · rw [hp', Polynomial.natDegree_zero]
    exact hp.bot_lt
  · rw [natDegree_lt_natDegree_iff hp']
    exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

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⁻¹ * (a - b)) = 1

Tactic:
← C_1

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = C 1
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
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                  ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
            else (0, p)).1
        else 0

Tactic:
rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)

Tactic:
rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ map f (r • p) = f r • map f p

Tactic:
rw [map, eval₂_smul, RingHom.comp_apply, C_mul']

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

Goal state before:
pp: case inr.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff p.natDegree = ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i

Tactic:
exact this _ le_rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - (a - eval a (C a)) * eval a (p /ₘ (X - C a)) = eval a p

Tactic:
eval_C,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - (a - a) * eval a (p /ₘ (X - C a)) = eval a p