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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
rw [this]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support
⊢ adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (⇑(of R M) '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤

Tactic:
rw [this]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: 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
⊢ q.leadingCoeff ≠ 0

Tactic:
exact mt Polynomial.leadingCoeff_eq_zero.1 hq0

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
⊢ ((aeval f) (q * p)) x = 0

Tactic:
aeval_mul,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
⊢ ((aeval f) q * (aeval f) p) x = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) (p * q)) y = 0

Tactic:
aeval_mul,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) p * (aeval f) q) y = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (p * q))) v = 0

Tactic:
aeval_mul,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) p' * (aeval f) (p * q)) v = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (q' * (p * q))) v = 0

Tactic:
aeval_mul,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) q' * (aeval f) (p * q)) v = 0
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Tactic:
rw [modEq_iff_dvd]
  exact exists_congr fun t => sub_eq_iff_eq_add'

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ d - c

Tactic:
rw [this]

Goal state after:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑b - ↑a = 0 ↔ a ≡ b [ZMOD ↑p]

Tactic:
← Int.cast_sub,

Goal state after:
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑(b - a) = 0 ↔ a ≡ b [ZMOD ↑p]
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
tsub_add_cancel_of_le h

Goal state after:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f m x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_1
α : 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)

Tactic:
rintro ⟨hr, H⟩ n hn
      rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
      · rwa [hM', hM, iterate_minimalPeriod]
      · exact H _ hM'

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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a + period m a * (n / period m a)) • a

Tactic:
pow_add,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| (m ^ (n % period m a) * m ^ (period m a * (n / period m a))) • a
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).const_mul _

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ x ∉ y :: l

Tactic:
simp [hy, hx]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ x ∉ y :: l

Tactic:
· simp [hy, hx]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card ↥s ∣ Nat.card α

Tactic:
by
  simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : Semiring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : StarModule R A
ι : Type u_3
inst✝ : Nonempty ι
S : ι → StarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subalgebra.coe_iSup_of_directed dir] using Subalgebra.isMulCommutative_iSup dir

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) = (y :: tail)[idxOf a (x :: y :: tail)]?

Tactic:
rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]

Goal state after:
case neg.ha
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ a ∈ (y :: tail).dropLast
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.prev a ha = l[(idxOf a l + (l.length - 1)) % l.length]

Tactic:
by
  cases l with | nil => grind | cons head tail =>
  by_cases ha₀ : a = head
  · subst ha₀
    simp
    grind
  rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
  congr
  rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
  all_goals grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev x hx = l'.prev x ⋯

Tactic:
by
  rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
  exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

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

Goal state before:
pp: α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l

Tactic:
lists,

Goal state after:
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ (Quotient.mk'' l).liftOn' (fun l ↦ ↑l.cyclicPermutations) ⋯ ↔ ↑l✝ = Quotient.mk'' l
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x

Tactic:
eq_zero_of_pow_eq_zero hx

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ primeFactorsList 0 = []

Tactic:
by rw [primeFactorsList]

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

Goal state before:
pp: ⊢ primeFactorsList 1 = []

Tactic:
by rw [primeFactorsList]

Goal state after:
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)
⊢ ∀ (x : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)),
    (Quotient.liftOn' x (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = x

Tactic:
intro q

Goal state after:
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 ω)
⊢ (Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = q
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)
⊢ ∀ (x : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))),
    Quotient.liftOn' (x.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = x

Tactic:
intro q

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
⊢ Quotient.liftOn' (q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = q
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1

Tactic:
intro q

Goal state after:
p : ℕ
hp : Prime p
n q : ℕ
⊢ q ∈ replicate n p → Prime q
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ a.primeFactorsList.Disjoint b.primeFactorsList

Tactic:
intro q

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ q ∈ a.primeFactorsList → q ∈ b.primeFactorsList → False
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
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)
⊢ Injective (Quotient.map' ⇑f ⋯)

Tactic:
simp_rw [← Quotient.eq''] at key

Goal state after:
case refine_1
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)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (f x) = Quotient.mk'' (f y)
⊢ Injective (Quotient.map' ⇑f ⋯)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
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)
⊢ Injective (Quotient.map' ⇑f ⋯)

Tactic:
simp_rw [← Quotient.eq''] at key
    refine Quotient.ind' fun x => ?_
    refine Quotient.ind' fun y => ?_
    exact (key x y).mpr

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ f.ker ≤ H

Tactic:
rw [f.ker_eq_bot hf.1]; exact bot_le

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

Goal state before:
pp: p n q : ℕ
h : n ≤ n + q
⊢ ↑p ^ (n + q) = 0

Tactic:
pow_add,

Goal state after:
p n q : ℕ
h : n ≤ n + q
⊢ ↑p ^ n * ↑p ^ q = 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (orbit G x).ncard = Nat.card X

Tactic:
orbit_eq_univ,

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ Set.univ.ncard = Nat.card X
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
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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

Goal state before:
pp: p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ p * m / (p * p) < p * m / p

Tactic:
rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]

Goal state after:
p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ m / p < m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
by
  rw [multiplicity, emultiplicity_eq_top.mpr h]
  decide

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

Goal state before:
pp: b f n : ℕ
l1 l2 : List Char
ih :
  ((n % b).digitChar :: l1).length = ((n % b).digitChar :: l2).length →
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih

Goal state after:
b f n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
ih :
  True →
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
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:
obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le' h

Goal state after:
n i b : ℕ
h : 2 ≤ b + 2
⊢ ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn0)

Goal state after:
case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ 0 < orderOf x ↔ IsOfFinOrder x

Tactic:
by
  rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

Goal state after:
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)
hL₁ : L.length = l + 1
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
have hL₂ : ∀ x ∈ L, x < b := ((mem_fixedLengthDigits_iff hb).mp hL).2

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
⊢ minimalPeriod (fun x ↦ 1 * x) 1 = minimalPeriod id 1

Tactic:
← one_mul_eq_id

Goal state after:
G : Type u_1
inst✝ : Monoid G
⊢ minimalPeriod (fun x ↦ 1 * x) 1 = minimalPeriod (fun x ↦ 1 * x) 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
hf : ∀ p ∈ n.factorization.support, Prime p
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n

pp: case mpr
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
hn : (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
⊢ f = (f.prod fun x1 x2 ↦ x1 ^ x2).factorization

Tactic:
exacts [prod_factorization_pow_eq_self hn, prod_pow_factorization_eq_self hf |>.symm]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList

Tactic:
intro q

Goal state after:
n p : ℕ
hp : Prime p
q : ℕ
⊢ q ∈ replicate (count p n.primeFactorsList) p →
    count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
factorization_factorial hp ((log_mono_right <| le_succ _).trans_lt hb),

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p + ∑ i ∈ Ico 1 b, n / p ^ i = #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i
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.factorization ≤ Finsupp.erase p n.factorization

Tactic:
intro q

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:

Tactic:
n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
pow_add,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ m * x ^ k = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization

Tactic:
intro q

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m * 1 ↔ m + k ≡ m [MOD orderOf x]

Tactic:
pow_add,

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ m * x ^ k = x ^ m * 1 ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ ↑(orderOf x) ∣ a - b ↔ x ^ a = x ^ b

Tactic:
by
  rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

Tactic:
rw [this]

Goal state after:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p ^ (n + m) = (x ^ p ^ n) ^ p ^ m

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ (p ^ n * p ^ m) = (x ^ p ^ n) ^ p ^ m
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1

Tactic:
· simp [n0]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case succ
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1) * a ∈ S * S

Tactic:
exact Set.mul_mem_mul ih ha

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 ≤ p.divX.degree

Tactic:
by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le)

Goal state after: