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

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p ∈ Ideal.span ↑s

Tactic:
rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) + q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
⊢ a % 0 = b % 0 ↔ a = b

Tactic:
emod_zero,

Goal state after:
a b : ℤ
⊢ a = b % 0 ↔ a = b
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

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

Goal state before:
pp: case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b

Tactic:
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

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

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
⊢ univSubsets = ↑Finset.univ.powerset.toList

Tactic:
simp only [Finset.coe_toList]

Goal state after:
case h.left
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
⊢ univSubsets = Finset.univ.powerset.val
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts ys l l' : List α
⊢ l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
induction ys generalizing l with

Goal state after:
case cons
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (permutationsAux2 t ts [] (y :: ys) fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
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 A
S : StarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S

Tactic:
exact
    ⟨fun h => Set.subset_union_left.trans h, fun h =>
      Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩

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

Goal state before:
pp: case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x

Tactic:
apply isPeriodicPt_zero

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x

Tactic:
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
by
  classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).length = minimalPeriod f x

Tactic:
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case add
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 A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : a ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p a x✝ ha hx✝
h₂ : p a y✝ ha hy✝
⊢ p a (x✝ + y✝) ha ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ minimalPeriod f x = p ∧ ¬minimalPeriod f x = 1

Tactic:
iff_self_and

Goal state after:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p → ¬minimalPeriod f x = 1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x t).length

Tactic:
simp [hl]

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

Goal state before:
pp: α : 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
⊢ m < as.length + 1

Tactic:
Nat.lt_succ_iff,

Goal state after:
α : 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
⊢ m ≤ as.length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : 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
⊢ n < bs.length + 1

Tactic:
Nat.lt_succ_iff,

Goal state after:
α : 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
⊢ n ≤ bs.length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
have : (n + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
this : (n + tl.length + 1) % (tl.length + 1) = n
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ Subsingleton (orbitRel.Quotient G α) ↔ Subsingleton (orbitRel.Quotient G α) ∧ Nonempty (orbitRel.Quotient G α)

Tactic:
iff_self_and

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ Subsingleton (orbitRel.Quotient G α) → Nonempty (orbitRel.Quotient G α)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
hs✝ : List α
hs : Nodup (Quotient.mk'' hs✝)
⊢ ∃ a, (fun l ↦ ⟨↑↑l, ⋯⟩) a = ⟨Quotient.mk'' hs✝, hs⟩

Tactic:
exact ⟨⟨_, hs⟩, by simp⟩

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

Goal state before:
pp: case cons.cons.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
hn.1,

Goal state after:
case cons.cons.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
⊢ IsChain r (b :: l ++ [b]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Data.List.Cycle

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

Tactic:
hn.1,

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x✝ : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
x : ↑(orbitRel.Quotient.orbit ω)
hx : ↑x ∈ orbitRel.Quotient.orbit ω
⊢ ⟦↑x⟧ = ω

Tactic:
rwa [orbitRel.Quotient.mem_orbit] at hx

Goal state after:
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
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
⊢ IsScalarTower (ZMod n) R M

Tactic:
exact ⟨fun x y z ↦ by rw [Algebra.smul_def, mul_smul]; rfl⟩

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

Goal state before:
pp: a : ℤ
⊢ a * a.sign = ↑a.natAbs

Tactic:
rw [Int.mul_sign_self]

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

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
    simp only [h, if_false] at this
    exact zero_lt_one.trans this

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j

Tactic:
by
  rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]

Goal state after:
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:
norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : Nontrivial G
⊢ n ≠ 1

Tactic:
rintro rfl
  obtain ⟨x, hx⟩ := exists_ne (0 : G)
  exact hx <| by simpa using char_nsmul_eq_zero 1 x

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

Goal state before:
pp: case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

pp: case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Tactic:
· intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert! this
    rw [ofDigits_digits]

Goal state after:
case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail

Tactic:
| cons hd tl =>

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

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

pp: case bit.true
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit true n) = List.map (fun b ↦ bif b then 1 else 0) (true :: n.bits)

Tactic:
· rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]

Goal state after:
case bit.true
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit true n) = List.map (fun b ↦ bif b then 1 else 0) (true :: n.bits)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (List.take (i + 1) (hd :: tl))

Tactic:
| cons hd tl =>

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n < multiplicity a b
⊢ ↑n < emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

Goal state after:
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:
Int.add_emod,

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 * ofDigits b L % ↑k) % ↑k
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:
Int.add_emod,

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' * ofDigits b' L % ↑k) % ↑k
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
Finset.disjiUnion_eq_biUnion,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).biUnion (consFixedLengthDigits hb l)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
have hL₁ : L.length = l + 1 := ((mem_fixedLengthDigits_iff hb).mp hL).1

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n k : ℕ
⊢ (n ^ k).factorization = k • n.factorization

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih =>
    rcases eq_or_ne n 0 with (rfl | hn)
    · simp
    rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ (x ^ orderOf x) ^ n = 1

Tactic:
pow_orderOf_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ 1 ^ n = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p = 1

Tactic:
apply Nat.eq_of_factorization_eq
  · exact pos_iff_ne_zero.mp (ordCompl_pos p (pow_ne_zero k hp.ne_zero))
  · exact one_ne_zero
  · simp [Prime.factorization_pow hp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:

Tactic:
x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ orderOf x) ^ i = 1

Tactic:
pow_orderOf_eq_one,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ 1 ^ i = 1
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0

Tactic:
· rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_single_mul_of_forall_add_ne]
    simpa [eq_comm] using h

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n

Tactic:
by
  nth_rw 2 [← prod_factorization_pow_eq_self hn]
  rw [eq_comm]
  apply Finset.prod_subset_one_on_sdiff
  · exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩
  · intro p hp
    obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
    rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
    simp [Finsupp.notMem_support_iff.mp hp2]
  · intro p hp
    simp [factorization_def n (prime_of_mem_primeFactors hp)]

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

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

Tactic:
prod_primeFactors_pow_factorization hn

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ∏ p ∈ n.primeFactors, p ^ n.factorization p ∣ ∏ x ∈ n.primeFactors, x ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ a.factorization p = (n • (factors.prod fun x1 x2 ↦ x1 ^ x2).factorization) p

Tactic:
prod_pow_factorization_eq_self foo

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ a.factorization p = (n • factors) p
Module: Mathlib.GroupTheory.OrderOfElement

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

pp: case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
⊢ p ∣ n → ↑n = 0

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

Goal state after:
case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
⊢ p ∣ n → ↑n = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * (C ↑p * X ^ (p - 1) * derivative X) =
    eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
C_eq_natCast,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1) * derivative X) =
    eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)

Tactic:
rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]

Goal state after:
case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Tactic:
exact Nat.le_add_right _ _

Goal state after: