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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
⊢ i < m ∨ j < n

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
⊢ ↑s ⊆ ↑(Subalgebra.restrictScalars R (adjoin S ↑s))

Tactic:
simp only [Subalgebra.coe_restrictScalars]

Goal state after:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
⊢ ↑s ⊆ ↑(adjoin S ↑s)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ∑ i ∈ d.support, d i * n ≤ m * n

Tactic:
rw [← Finset.sum_mul]

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ (∑ i ∈ d.support, d i) * n ≤ m * n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ C (coeff m f) ∈ Ideal.map C I

Tactic:
apply Ideal.mem_map_of_mem _

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ coeff m f ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ -b - -a = -(b - a)

Tactic:
lia

Goal state after:
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:
← modEq_neg,

Goal state after:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -(c * a) ≡ -(c * b) [ZMOD -(c * n)]
Module: Mathlib.Data.Int.ModEq

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

Tactic:
lia

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]
⊢ d - c = b + d - (a + c) - (b - a)

Tactic:
lia

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

Goal state before:
pp: case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(m.gcd c)

Tactic:
exact Int.ediv_dvd_ediv (gcd_dvd_left ..) h

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD ↑n.natAbs] ↔ a ≡ b [ZMOD n]

Tactic:
simp [natCast_natAbs]

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

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
p : ℕ
hp : Prime p
hn : p ∣ n
hm : p ∣ m
⊢ 0 < m

Tactic:
lia

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

Goal state before:
pp: R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
⊢ factorₐ R ⋯ = AlgHom.id R (A ⧸ I)

Tactic:
ext
  simp

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
p q : StarSubalgebra R A
h : (fun S ↦ S.carrier) p = (fun S ↦ S.carrier) q
⊢ p = q

Tactic:
obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ 1 ≤ n

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at x_mem
  by_cases h : x = y
  · rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
  · rw [nextOr, nextOr, IH]
    simpa [h] using x_mem

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : m < n
⊢ 0 < n - m

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ 0 < m - n

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ Injective f

Tactic:
rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]

Goal state after:
α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ periodicPts f ⊆ range f
Module: Mathlib.Data.List.Cycle

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

Tactic:
cases l <;> simp [prev, hx]

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

Goal state before:
pp: case cons.left
α : 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
ys : List α
hy : ys ∈ l.permutations'
⊢ (permutations'Aux x ys).Nodup

Tactic:
rw [mem_permutations'] at hy

Goal state after:
case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ (permutations'Aux x ys).Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ 0 < l.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.length - 1 - k < l.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length

Tactic:
by
  obtain ⟨x, y, hxy, hx, hy⟩ := h
  induction s using Quot.inductionOn with | _ l
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp at hx
  · simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
    simp [hx, hy] at hxy
  · simp [Nat.succ_le_succ_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : Monoid X
inst✝¹ : MulAction X G
H : Subgroup G
inst✝ : QuotientAction X H
b : X
q : G ⧸ H
⊢ ↑(b • Quotient.out q) = b • q

Tactic:
by rw [← Quotient.smul_mk, QuotientGroup.out_eq']

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose⁻¹ * g = 1

Tactic:
rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq G (g⁻¹ • x) x).choose_spec]

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

Goal state before:
pp: ⊢ primeFactors 0 = ∅

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ g ∈ H

Tactic:
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ Nat.card ((G ⧸ K) × ↥K ⧸ H.subgroupOf K) = Nat.card (G ⧸ H)

Tactic:
Nat.card_congr <| quotientEquivProdOfLE h

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]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ 0 < n₂ - n₁

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ n₂ - n₁ ≤ H.index

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ ↑(n₂ - n₁) = ↑n₂ + -↑n₁

Tactic:
lia

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

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ z + 0 * ↑k = z

Tactic:
zero_mul,

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ z + 0 = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z.cast + 0 * ↑k = z

Tactic:
zero_mul,

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z.cast + 0 = z
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ ¬n = 0

Tactic:
lia

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

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
· rw [← h]; apply ZMod.val_lt

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 0 = ∅

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 0 = ∅

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 1 = {1}

Tactic:
ext
  simp

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + 0 * ↑(a.val.gcdB n.succ)

Tactic:
zero_mul,

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ 0 ≤ (divisors 0).sup id

Tactic:
apply zero_le

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 0 = ∅

Tactic:
ext
  simp

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

Goal state before:
pp: p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ d = 0 → p = 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
rw [properDivisors_zero, subset_empty] at hsub
    simp [hsub]

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ 1

Tactic:
lia

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 1 ≤ b

Tactic:
lia

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

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < m

Tactic:
lia

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

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ (0 < n1 ∧ 1 ≤ n2) ∧ 0 < n2 ∧ 1 ≤ n1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisors = z.divisors

Tactic:
ext
  simp

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

Goal state before:
pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1

Tactic:
refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ 2 * a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 0 < 2 * n

Tactic:
lia

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

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

Tactic:
by rw [choose_succ_right_eq, choose_mul_succ_eq]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
rw [neg_val']
  by_cases h : a = 0; · rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
  rw [if_neg h]
  apply Nat.mod_eq_of_lt
  exact Nat.sub_lt (NeZero.pos n) (val_pos.mpr h)

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

Goal state before:
pp: x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1

Tactic:
by simp [centralBinom, choose]

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

Goal state before:
pp: x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2

Tactic:
by simp [centralBinom, choose]

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

Goal state before:
pp: x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3

Tactic:
by simp [centralBinom, choose]

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✝¹ : NeZero n
inst✝ : Nontrivial G
this✝ : n ≠ 0
this : n ≠ 1
⊢ 2 ≤ n

Tactic:
lia

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

Goal state before:
pp: p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ 1 < p + 2

Tactic:
lia

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

Goal state before:
pp: case ind.succ.tail.a.hLtN
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 0 < n + 1

Tactic:
lia

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

Goal state before:
pp: case ind.succ.tail.a.hLtK
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 1 < b + 2

Tactic:
lia

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

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

Goal state before:
pp: case e'_2.a
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

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

Goal state before:
pp: case e'_3
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b

Tactic:
by
  simp [emultiplicity]

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

Goal state before:
pp: b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ b = 0

Tactic:
lia

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

Goal state before:
pp: b : ℕ
h : b ≠ 1
hb : ¬1 < b
n✝ : ℕ
⊢ b = 0

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : b + 2 ≤ 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n ≠ 1

Tactic:
lia

Goal state after:
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 ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p

Tactic:
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
                simp_all [mul_comm, mul_left_comm, pow_add]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
orderOf_dvd_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ (x ^ n) ^ orderOf x = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
rw [h0, coprime_zero_right] at h
    exact ⟨1, by rw [h, pow_one, pow_one]⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ 1 < orderOf x

Tactic:
lia

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ p ∣ b

Tactic:
simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℤ
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
⊢ orderOf (x * y) = orderOf y

Tactic:
have hxy := dvd_of_forall_prime_mul_dvd hdvd

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

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

pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
· have hdisj : Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
        {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
      simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
    rw [factorization_choose hp hkn (lt_succ_self _), factorization_eq_card_pow_dvd_of_lt hp
      hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt), log_pow hp.one_lt,
      ← card_union_of_disjoint hdisj, filter_union_right]
    have filter_le_Ico := (Ico 1 n.succ).card_filter_le
      fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
    rwa [card_Ico 1 n.succ] at filter_le_Ico

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

Tactic:
lia

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

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p ∈ Finset.range (n + 1)

Tactic:
rw [Finset.mem_range]

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p < n + 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n : ℕ
⊢ n ≤ 2 * n

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
⊢ IsOfFinOrder a

Tactic:
obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ IsOfFinOrder a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ (↑(powers a)).Finite ↔ IsOfFinOrder a

Tactic:
by
  refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
  obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])
  refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
  rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

Goal state after:
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 k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

Tactic:
lia

Goal state after:
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 k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n

Tactic:
lia

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
lia

Goal state after:
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 k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ p ^ n - k ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
⊢ IsOfFinOrder a

Tactic:
obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ IsOfFinOrder a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ ↑i = 1

Tactic:
orderOf_dvd_iff_pow_eq_one,

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ x ^ i = 1 ↔ x ^ ↑i = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ^ i ∣ n
⊢ i ≠ 0

Tactic:
lia

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

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n ≠ 0

Tactic:
lia

Goal state after: