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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
⊢ (f.sum fun n a ↦ C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
refine Submodule.sum_mem _ fun n _hn => ?_

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ (fun n a ↦ C a * X ^ n) n (f.coeff n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case e'_1.e'_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ (renameEquiv R (Fintype.equivFin σ)) (C r) = C r

Tactic:
simp only [renameEquiv_apply, algHom_C, algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ ι x f, Surjective ⇑f

Tactic:
rw [iff_quotient_mvPolynomial]

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
⊢ (RingHom.id A).FiniteType

Tactic:
simp [FiniteType]; infer_instance

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

Goal state before:
pp: case refine_1.inr
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ toSubmodule S * toSubmodule T

Tactic:
← one_mul x

Goal state after:
case refine_1.inr
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ 1 * x ∈ toSubmodule S * toSubmodule T
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) ⊥ ↔ x✝ ∈ I

Tactic:
mem_comap,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ (Quotient.mk I) x✝ ∈ ⊥ ↔ x✝ ∈ I
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
this : 1 ∣ x
h : y = x
⊢ x = x ∧ y = x

Tactic:
subst h

Goal state after:
case inl
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy hx : y ≠ 1
hp : Prime y
h : x * y✝ = y ^ 2
pdvdxy : y ∣ x * y✝
this : 1 ∣ y
⊢ y = y ∧ y = y
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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : r₁ - r₂ ∈ comap (algebraMap R A) P
⊢ r₁ • a₁ ≈ r₂ • a₂

Tactic:
mem_comap,

Goal state after:
R✝ : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : (algebraMap R A) (r₁ - r₂) ∈ P
⊢ r₁ • a₁ ≈ r₂ • a₂
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys ?f').snd = (permutationsAux2 t ts [] ys f).snd

pp: case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β

pp: case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = ?f' (map id a)

Tactic:
· rfl

Goal state after:
case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f^[n] x = x

Tactic:
hx.eq

Goal state after:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ x = x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
· rfl

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_2
α : 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)

Tactic:
nth_rw 2 [← hM]

Goal state after:
case pos.refine_2
α : 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x - succ 0 + succ 0] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations'.Nodup

Tactic:
induction hs with

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

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

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])

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

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

Tactic:
· rfl

Goal state after:
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])

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

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦[]⟧

pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧

Tactic:
· rfl

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
⊢ (comap f H).index = H.index

Tactic:
have key : ∀ x y : G',
      QuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) := by
    simp only [QuotientGroup.leftRel_apply]
    exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ (comap f H).index = H.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast

Tactic:
· rfl

Goal state after:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Tactic:
· rfl

Goal state after:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
⊢ (⨅ i, f i).index ≠ 0

Tactic:
simp_rw [← relIndex_top_right] at hf ⊢
  exact relIndex_iInf_ne_zero hf

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

Goal state before:
pp: case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
· rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ H.index ≠ 0

Tactic:
rw [index_eq_card]

Goal state after:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℕ
h : a = b
x : ZMod a
⊢ ((ringEquivCongr h) x).val = x.val

Tactic:
subst h

Goal state after:
a : ℕ
x : ZMod a
⊢ ((ringEquivCongr ⋯) x).val = x.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ (-1).val = n

Tactic:
dsimp [val, Fin.val_neg']
  cases n
  · simp
  · dsimp [ZMod, ZMod.cast]
    rw [Fin.coe_neg_one]

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

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

Tactic:
Int.mul_sign_self

Goal state after:
a : ℤ
⊢ ↑a.natAbs = ↑a.natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val.Coprime (n + 1)

Tactic:
apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ IsUnit ↑m ↔ m.Coprime n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩

Goal state after:
m n : ℕ
H : IsUnit ↑m
⊢ m.Coprime n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : NeZero n
x y : G
⊢ IsPeriodicPt (fun x_1 ↦ x + x_1) n y

Tactic:
simpa [char_nsmul_eq_zero, IsPeriodicPt] using! isFixedPt_id _

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

Goal state before:
pp: case zero.zero
⊢ ofDigits 0 (digits 0 0) = 0

pp: case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Tactic:
· rfl

Goal state after:
case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
| ind n h =>

Goal state after:
case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
⊢ maxPowDvdDiv 1 1 = (0, 1)

Tactic:
simp [maxPowDvdDiv_of_not_dvd, *]

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

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 1
⊢ p.maxPowDvdDiv 1 = (0, 1)

Tactic:
simp [maxPowDvdDiv_of_not_dvd, *]

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

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
by
  have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
  convert! @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)
  rw [ofDigits_digits]

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

Goal state before:
pp: case inr.inr.nil
p : ℕ
h : p < 1
h_nonempty : [] ≠ []
h_ne_zero : [].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [], l < p
⊢ 0 = ofDigits 0 [] - [].sum

pp: case inr.inr.cons
p : ℕ
h : p < 1
head✝ : ℕ
tail✝ : List ℕ
h_nonempty : head✝ :: tail✝ ≠ []
h_ne_zero : (head✝ :: tail✝).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ head✝ :: tail✝, l < p
⊢ 0 = ofDigits 0 (head✝ :: tail✝) - (head✝ :: tail✝).sum

Tactic:
· rfl

Goal state after:
case inr.inr.cons
p : ℕ
h : p < 1
head✝ : ℕ
tail✝ : List ℕ
h_nonempty : head✝ :: tail✝ ≠ []
h_ne_zero : (head✝ :: tail✝).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ head✝ :: tail✝, l < p
⊢ 0 = ofDigits 0 (head✝ :: tail✝) - (head✝ :: tail✝).sum
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

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! = ofDigits b (b.digits (n + 1)) % b

Tactic:
Nat.ofDigits_mod_eq_head! _ _

Goal state after:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : emultiplicity a b < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
by
  unfold emultiplicity at hm
  split at hm
  · simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)
  · simp at hm

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

Goal state before:
pp: n i b : ℕ
h : 2 ≤ b
⊢ (b.digits n).getD i 0 = n / b ^ i % b

Tactic:
by
  obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le' h
  clear h
  rw [List.getD_eq_getElem?_getD]
  induction n using Nat.caseStrongRecOn generalizing i with
  | zero => simp
  | ind n IH =>
    rcases i with _ | i
    · rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp
    · simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
by
  rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity, ← padicValNat_def' ha.ne_one hb,
    Nat.cast_le]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
by
  rw [factorization_eq_primeFactorsList_multiset n]
  simp only [← prod_toMultiset, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]
  exact prod_primeFactorsList hn

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

Goal state before:
pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

Tactic:
subst h

Goal state after:
case refine_2
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
x✝ : d ∣ d * c
⊢ d.factorization ≤ (d * c).factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ n.factorization = 0 ↔ n = 0 ∨ n = 1

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]
  simp [Multiset.coe_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

pp: case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n

Tactic:
· rfl

Goal state after:
case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ⟨x ^ n, ⋯⟩ = (finEquivPowers hx) ⟨n % orderOf x, ⋯⟩

Tactic:
finEquivPowers_apply,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ⟨x ^ n, ⋯⟩ = ⟨x ^ ↑⟨n % orderOf x, ⋯⟩, ⋯⟩
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)

Tactic:
rw [h.add_pow_prime_pow_eq' hp, mul_assoc _ x, mul_assoc, mul_sum _ _ (_ * _)]
  congr! 3 with k hk
  obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
  rw [← mul_pow_sub_one (by lia), ← mul_pow_sub_one (n := p ^ n - k) (by lia)]
  rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).coeff d = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
    · exact natDegree_mul_le_of_le ‹_› ‹_›
    · exact ne_comm.mp h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX

Tactic:
by rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(p.natTrailingDegree + q.natTrailingDegree) = ↑p.natTrailingDegree + ↑q.natTrailingDegree

Tactic:
apply WithTop.coe_add

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0

Tactic:
· rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
⊢ 0 < 1 * p.natDegree

Tactic:
rwa [one_mul]

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0

Tactic:
subst h

Goal state after:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
⊢ (⇑derivative)^[x] p = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ¬∃ x, p.IsRoot x
⊢ ∀ (a : R), count a 0 = rootMultiplicity a p

Tactic:
intro a
        rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x ((s • 1) • p) = s • eval x p

Tactic:
eval,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval₂ (RingHom.id R) x ((s • 1) • p) = s • eval x p
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree ≠ q.natDegree

Tactic:
· contrapose h0
    rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]
    simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
    rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]

Goal state after: