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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) (1 * 1) =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) (1 * 1) =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) (1 * 1) = single (m₁ * m₂) 1

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) 1 = single (m₁ * m₂) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) (1 * 1) = single (m₁ * m₂) 1

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) 1 = single (m₁ * m₂) 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ p = eval₂ (ϕ.comp C) (fun s ↦ ϕ (X s)) p

Tactic:
refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_

Goal state after:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s ↦ ϕ (X s)) p
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)

Tactic:
by
  rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]

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

Goal state before:
pp: case prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (R × S) p

Tactic:
obtain _ | _ := ‹ExpChar S p›

Goal state after:
case prime.zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero S
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
hp : Nat.Prime 1
hchar✝ : CharP R 1
⊢ ExpChar (R × S) 1

case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + y ^ 2

Tactic:
simp [add_pow_two]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ (↑m.toList).lists → x ≤ n.val.lists → x ≤ ⊥) ↔ ¬m = n

Tactic:
← n.coe_toList,

Goal state after:
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ (↑m.toList).lists → x ≤ (↑n.toList).lists → x ≤ ⊥) ↔ ¬m = n
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
comp_iterate_pred_of_pos f hn,

Goal state after:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f^[n] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + 1 * r

Tactic:
one_mul

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ ∃ x, l₁ ++ [t] ++ ts = l₁ ++ t :: ts

Tactic:
by simpa using p

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) • a = m ^ n • a

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]

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

Goal state before:
pp: case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = permutations'Aux t x✝

Tactic:
permutations'Aux_eq_permutationsAux2,

Goal state after:
case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = (permutationsAux2 t [] [x✝ ++ [t]] x✝ id).snd
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ k • (a - b) = 0

Tactic:
smul_sub,

Goal state after:
M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ k • a - k • b = 0
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Tactic:
· have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
    exact Quotient.eq''.mp h

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [isPrimePow_nat_iff]
  refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩
  rintro ⟨p, k, hp, hk, rfl⟩
  refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩
  conv => {lhs; rw [← (pow_one p)]}
  exact Nat.pow_le_pow_right hp.one_lt.le hk

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

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

Tactic:
simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ (a :: l₁).prod

Tactic:
rw [prod_cons]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ a * l₁.prod
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p

Tactic:
exact h₂

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

Goal state before:
pp: n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList <+ k.primeFactorsList

Tactic:
obtain ⟨a, rfl⟩ := h

Goal state after:
n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
· exact Or.inr ⟨p, hp, hdvd, hodd⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H * H.index = Nat.card G

Tactic:
by
  rw [← relIndex_bot_left, ← index_bot]
  exact relIndex_mul_index bot_le

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

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a

Tactic:
· apply Fin.cast_val_eq_self

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1

Tactic:
exact Nat.lt_of_sub_eq_succ rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : H.IsFiniteRelIndex L
h : H ≤ K
⊢ K.IsFiniteRelIndex L

Tactic:
by
  rw [isFiniteRelIndex_iff_finiteIndex] at *
  exact finiteIndex_of_le <| subgroupOf_mono L 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'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
by
  rw [normalCore_eq_ker]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r

Goal state after:
case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ℕ
⊢ ↑r • 1 * x = ↑r • x ∧ x * ↑r • 1 = ↑r • x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
by
  obtain ⟨a, b⟩ := x
  simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
    Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]
  constructor
  · rintro ⟨han, ⟨ha, han'⟩, rfl⟩
    simp [Nat.mul_div_eq_iff_dvd, han]
    lia
  · rintro ⟨rfl, hab⟩
    rw [mul_ne_zero_iff] at hab
    simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

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

Goal state before:
pp: n : ℤ
⊢ ↑n = 1 ↔ Odd n

Tactic:
← Int.cast_one,

Goal state after:
n : ℤ
⊢ ↑n = ↑1 ↔ Odd n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n✝ n x : ℕ
h : x.Coprime n
⊢ (↑x)⁻¹ * ↑x = 1

Tactic:
by rw [mul_comm, coe_mul_inv_eq_one x h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
a✝ : ℕ
⊢ (a✝ = 1 ∨ a✝ = p) ∧ p ≠ 0 ↔ a✝ ∈ {1, p}

Tactic:
and_iff_left pp.ne_zero,

Goal state after:
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ ∈ {1, p}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

Tactic:
simp [divisorsAntidiag]
    grind [Nat.cast_inj]

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

Goal state before:
pp: m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero <| by rintro (rfl : n = 0); simp at h
  exact Fin.val_cast_of_lt h

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
r : ZMod (n + 1)
m : M
⊢ r • m = r • m

Tactic:
obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r

Goal state after:
case succ
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
m : M
r : ℕ
⊢ ↑r • m = ↑r • m
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
induction n using Nat.strongRecOn with

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 inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
have hk : k = (p.maxPowDvdDiv n).1 := by
      · apply Nat.le_antisymm
        · rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
          apply Nat.le_refl
        · rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]
          apply Nat.le_refl

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by
  simp [lt_top_iff_ne_top, emultiplicity_eq_top]

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

Goal state before:
pp: n i b : ℕ
⊢ ((b + 2).digits n)[i]?.getD 0 = n / (b + 2) ^ i % (b + 2)

Tactic:
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.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
⊢ ¬Prime p ∨ ¬p ∣ n ∨ ¬n ≠ 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
not_ne_iff

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
h' : IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ False

Tactic:
exact h1 ⟨n, h, h'⟩

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

Goal state before:
pp: case succ
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

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

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ 1 * x = x

Tactic:
one_mul

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x = x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf y

Tactic:
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred * (x * y))
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
one_mul

Goal state after:
n k p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n / p ^ n.factorization p
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
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n

Tactic:
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

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ (n.choose k).factorization p = 0

Tactic:
factorization_choose_eq_zero_of_lt hp

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ 0 = 0
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 ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
simp_rw [Icc_eq_cons_Ico zero_le, Ico_eq_cons_Ioo (pow_pos hp.pos _)]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ x_1 ∈ cons (p ^ n) (cons 0 (Ioo 0 (p ^ n)) ⋯) ⋯, x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1) =
    x ^ p ^ n + y ^ p ^ n + ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑((p ^ n).choose x_1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
· exact absurd (zero_dvd_iff.mp hea) ha_pos

Goal state after:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

pp: case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
· exact fun h => False.elim <| h rfl

Goal state after:
case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Algebra.MonoidAlgebra.Division

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

Tactic:
coeff_modOf_of_not_exists_add x _ _ h,

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