mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).Monic

Tactic:
rw [Monic, leadingCoeff, p.natDegree, p.2.1]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : WithBot ℕ
hl : ∀ p ∈ l, p.degree ≤ n
⊢ l.sum.degree ≤ n

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [List.mem_cons, forall_eq_or_imp] at hl
    rcases hl with ⟨hhd, htl⟩
    rw [List.sum_cons]
    exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
degree_eq_natDegree h

Goal state after:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ↑p.natDegree ≤ (List.map natDegree l).maximum
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
Polynomial.degree,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).support.max = ↑(degreeOf 0 f)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ 0 + y ^ 0 = (x + y) ^ 0

Tactic:
zero_add,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ y ^ 0 = (x + y) ^ 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by_cases hb₀ : b = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ f ∈ degreeLT R n ↔ f.degree < ↑n

Tactic:
simpa [degreeLT, Submodule.mem_iInf] using (degree_lt_iff_coeff_zero _ _).symm

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

Goal state before:
pp: case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ map C P ≠ ⊤

Tactic:
rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]
      use 0
      rw [coeff_one_zero, ← eq_top_iff_one]
      exact h.1

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

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ ((∃ n, f.coeff n ∉ P) ∧ ∃ n, g.coeff n ∉ P) → ∃ n, (f * g).coeff n ∉ P

Tactic:
rintro ⟨hf, hg⟩

Goal state after:
case mem_or_mem'
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
⊢ ∃ n, (f * g).coeff n ∉ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]

Goal state after:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r
Module: Mathlib.RingTheory.Polynomial.Basic

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

pp: case convert_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Type ?u.42

pp: case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
· congr!
    simp only [renameEquiv_apply, algHom_C, algebraMap_eq]

Goal state after:
case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ (adjoin R t).FG

Tactic:
exact ⟨h.toFinset, by simp⟩

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

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a) + ↑a = 0 + ↑a

Tactic:
zero_add,

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a) + ↑a = ↑a
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

Tactic:
rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ (Set.range fun x ↦ if Even x then 0 else 1) = {0, 1}

Tactic:
Set.range_ite_const

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ {0, 1} = {0, 1}

case hp
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, Even a

case hn
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, ¬Even a
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ (Set.range fun x ↦ if Even x then 0 else 1) = {0, 1}

Tactic:
Set.range_ite_const

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ {0, 1} = {0, 1}

case hp
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ∃ a, Even a

case hn
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ∃ a, ¬Even a
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
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier

Tactic:
simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
    rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
    simpa using ha

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
hx : (Quotient.mk (I ^ (n + 1))) y ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ ∃ a,
    (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨(Quotient.mk (I ^ (n + 1))) y, hx⟩

Tactic:
refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
hx : (Quotient.mk (I ^ (n + 1))) y ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) (Submodule.Quotient.mk ⟨y, hy⟩) =
    ⟨(Quotient.mk (I ^ (n + 1))) y, hx⟩
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ ↑n • a = a ↔ ↑(period g a) ∣ ↑n

Tactic:
rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod (fun x ↦ a • x) b ∣ n

Tactic:
← period_eq_minimalPeriod,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ period a b ∣ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod (fun x ↦ a • x) b) ∣ n

Tactic:
← period_eq_minimalPeriod,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(period a b) ∣ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ (n % minimalPeriod (fun x ↦ a • x) b) • b = a ^ n • b

Tactic:
← period_eq_minimalPeriod,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ (n % period a b) • b = a ^ n • b
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ (n % ↑(minimalPeriod (fun x ↦ a • x) b)) • b = a ^ n • b

Tactic:
← period_eq_minimalPeriod,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ (n % ↑(period a b)) • b = a ^ n • b
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
inst✝ : Fintype α
⊢ minimalPeriod f x ≤ card α

Tactic:
← periodicOrbit_length

Goal state after:
α : Type u_1
f : α → α
x : α
inst✝ : Fintype α
⊢ (periodicOrbit f x).length ≤ card α
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Tactic:
by
  rw [minimalPeriod_prodMap]; exact Nat.dvd_lcm_right _ _

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (if x = z then y else (z :: head✝ :: tail✝).prev x ⋯) = y

Tactic:
if_pos hz

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ y = y
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

Tactic:
have ⟨_, _⟩ := l.dropLast_prefix
    grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.next l ⋯ = l.rotate 1

Tactic:
apply List.ext_getElem
  · simp
  · intros
    rw [getElem_pmap, getElem_rotate, next_getElem _ h]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
⊢ ∀ (h₂ : n < (l.rotate (l.length - 1)).length), (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]

Tactic:
hn'

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.1 ∈ orbit M y.1

Tactic:
rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.2 ∈ orbit M y.2

Tactic:
rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
by simpa [Iff.comm] using h a

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

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

Tactic:
induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

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

Goal state before:
pp: case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

Tactic:
exact one_dvd _

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ cast 0 = 0

Tactic:
delta ZMod.cast

Goal state after:
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #{g | f g = f x} = #{g | f g = f y}

Tactic:
rcases mul_left_surjective x y with ⟨y, rfl⟩

Goal state after:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #{g | f g = f x} = #{g | f g = f ((fun x_1 ↦ x * x_1) y)}
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g = f' x * ↑(f'.toHomUnits y) ↔ f' g = f' x * f' y

Tactic:
f'.coe_toHomUnits

Goal state after:
case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g = f' x * f' y ↔ f' g = f' x * f' y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1

Tactic:
val_one_eq_one_mod

Goal state after:
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ {p, 1}.erase p = {1}

Tactic:
erase_insert fun con => pp.ne_one (mem_singleton.1 con)

Goal state after:
p : ℕ
pp : Prime p
⊢ {1} = {1}
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.choose k < n.descFactorial k

Tactic:
by
  rw [choose_eq_descFactorial_div_factorial]; exact Nat.div_lt_self (by simpa) (by simpa)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
⊢ a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
by
  simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b ∈ {0, 1, 2, 3, 4} ↔
    (a, b) ∈
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
by
  simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g

Tactic:
by
    rw [RingEquiv.coe_ringHom_inj_iff]
    apply RingHom.ext_zmod _ _

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

Goal state before:
pp: b k : ℕ
l : List ℕ
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l

Tactic:
ofDigits_append

Goal state after:
b k : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d

Tactic:
ofDigits_append

Goal state after:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ p.maxPowDvdDiv p = (1, 1)

Tactic:
by
  simpa using maxPowDvdDiv_base_pow hp 1

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

Goal state before:
pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ n / b.succ.succ ≠ 0

Tactic:
← pos_iff_ne_zero

Goal state after:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ 0 < n / b.succ.succ
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
⊢ 0 + ofDigits p tl = ofDigits p (hd :: tl).tail

Tactic:
zero_add,

Goal state after:
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 tl = ofDigits p (hd :: tl).tail
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1 + 1) * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
Nat.sub_add_cancel (one_le_of_lt h),

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ p * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b

Tactic:
exact one_dvd _

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

Goal state before:
pp: case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b ^ (0 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
zero_add,

Goal state after:
case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b ^ 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (ψ x) ∣ orderOf x

Tactic:
apply orderOf_dvd_of_pow_eq_one

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ x ^ orderOf x = 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
← factorization_le_iff_dvd ?_ hn,

Goal state after:
case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization ≤ n.factorization

n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 2)

Tactic:
rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / (p ^ a.factorization p * p ^ b.factorization p) = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

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)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + (0 + (1 + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
zero_add,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + (1 + (n + 1).factorization p) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

Goal state after: