mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ m * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
← pow_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ (m + (n - m))) = x ^ n - x ^ m * y ^ (n - m)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
⊢ ↑(p.restriction.coeff p.natDegree) = 1

Tactic:
rw [H, OneMemClass.coe_one]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f

Tactic:
rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S ≤ map f ⊤
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
⊢ Algebra.adjoin R s ⊔ Algebra.adjoin R s' = S ⊔ S'

Tactic:
hs.2,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
⊢ S ⊔ Algebra.adjoin R s' = S ⊔ S'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), C (f.coeff i) ∈ I
⊢ Ideal.span {g | ∃ i, C (f.coeff i) = g} ≤ I

Tactic:
exact (Ideal.span_le.trans range_subset_iff).mpr cf

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

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

Tactic:
let p := Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }
  nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]
  refine Submodule.sum_mem _ fun n _hn => ?_
  dsimp
  have : C (coeff f n) ∈ p := by
    apply subset_span
    rw [mem_ofPred_eq]
    use n
  have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
  convert! this using 1
  simp only [monomial_mul_C, one_mul, smul_eq_mul]
  rw [← C_mul_X_pow_eq_monomial]

Goal state after:
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:
apply mul_le_mul' (.trans _ hF) le_rfl

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 ≤ F.totalDegree
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a

Tactic:
exact (dvd_mul_left n m).trans h

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 - a) * (c / ↑d)

Tactic:
← Int.mul_ediv_assoc (b - a) (gcd_dvd_right ..),

Goal state after:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ (b - a) * c / ↑(m.gcd c)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b m n : ℤ
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD ↑(m.lcm n)]

Tactic:
simp only [modEq_iff_dvd, coe_lcm_dvd_iff]

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (ker f)

pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)

Tactic:
· intro hx
    obtain ⟨y, hy⟩ := Quotient.mk_surjective x
    rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
    rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
    exact ⟨y, hx, rfl⟩

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + b + b = a

Tactic:
add_assoc,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + (b + b) = a
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Tactic:
isPeriodicPt_iff_minimalPeriod_dvd,

Goal state after:
α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), minimalPeriod f x ∣ n ↔ minimalPeriod g y ∣ n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + (1 + tl.length)) % (tl.length + 1) = n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + tl.length + 1) % (tl.length + 1) = n

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + (tl.length + 1)) % (tl.length + 1) = n
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:
← next_reverse_eq_prev _ hn,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.prev x ⋯
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ (p ^ k).minFac = p

Tactic:
by
  rw [Nat.pow_minFac hk, hp.minFac_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
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
⊢ ↑x ∈ orbitRel.Quotient.orbit ω

Tactic:
have hx := x.property
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
    rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]

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
q : orbitRel.Quotient (↥H) X
⊢ ∀ (a b : X), (orbitRel (↥H) X) a b → ↑⋯.choose = ↑⋯.choose

Tactic:
intro y₁

Goal state after:
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
q : orbitRel.Quotient (↥H) X
y₁ : X
⊢ ∀ (b : X), (orbitRel (↥H) X) y₁ b → ↑⋯.choose = ↑⋯.choose
Module: Mathlib.GroupTheory.GroupAction.Quotient

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

Tactic:
refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)

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 ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (castHom ⋯ R) ↑k = 0 → ↑k = 0

Tactic:
rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)

Tactic:
cases a <;> rfl

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

Goal state before:
pp: a : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
cases a <;> rfl

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

Goal state before:
pp: a : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
cases a <;> rfl

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

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

Tactic:
cases a <;> rfl

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

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ x✝ ∈ AddSubgroup.zmultiples ↑n

Tactic:
rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ (List.filterMap
        (fun x ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)).toFinset =
    n.divisorsAntidiagonal

Tactic:
divisorsAntidiagonal,

Goal state after:
n : ℕ
⊢ (List.filterMap
        (fun x ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)).toFinset =
    filterMap
      (fun x ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
by
        push_cast
        rw [natCast_zmod_val]
        rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := (n + 1).divisorsAntidiagonal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +contextual [s, disjoint_left, eq_comm, forall_comm (α := _ * _ = _)]

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

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

Tactic:
add_assoc,

Goal state after:
n : ℕ
⊢ 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + (n + 1) - n))
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ (n + 1).Coprime (n + n + 1)

Tactic:
add_assoc,

Goal state after:
n : ℕ
⊢ (n + 1).Coprime (n + (n + 1))
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]

Tactic:
rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

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

Goal state before:
pp: b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
List.append_assoc,

Goal state after:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ (List.replicate k 0 ++ b.digits m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑(multiplicity a b)

Tactic:
cases hm : emultiplicity a b

Goal state after:
case top
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
hm : emultiplicity a b = ⊤
⊢ ⊤ = ↑(multiplicity a b)

case coe
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
a✝ : ℕ
hm : emultiplicity a b = ↑a✝
⊢ ↑a✝ = ↑(multiplicity a b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k = (↑d + b' * ofDigits b' L) % ↑k

Tactic:
conv_rhs => rw [Int.add_emod, Int.mul_emod]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
by
  ext p
  simp only [add_apply, ← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p, count_append]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
refine ⟨fun hL ↦ ?_, ?_⟩

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 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
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
add_assoc,

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
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1 + 1)) * s * p
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 + ∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), i.factorization p =
    (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
add_assoc,

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 + ∑ i ∈ Ico (p * n + 1) (p * (n + 1) + 1), i.factorization p =
    (p * n)!.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hd
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
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p = 1

Tactic:
← Nat.dvd_one,

Goal state after:
case hd
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
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p ∣ 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1

Tactic:
← Nat.dvd_one,

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a ∣ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ m * a ^ (n - m) = a ^ m * 1

Tactic:
← pow_add,

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
⊢ a ^ (m + (n - m)) = a ^ m * 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x + y) ^ (p * (n / p))

Tactic:
← pow_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p + p * (n / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
← sub_pow_expChar_of_commute _ h,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))

Tactic:
← pow_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p + p * (n / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) + y ^ p - y ^ p

Tactic:
add_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + (↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) + y ^ p) - y ^ p
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rcases p with - | p

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

case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1

Tactic:
← Nat.dvd_one,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) ∣ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
by
  use Fintype.card (G ⧸ zpowers x)
  rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]

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

Goal state before:
pp: case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
← Nat.primeFactors_pow k hm

Goal state after:
case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ (k ^ m).primeFactors
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ card ↑(S ^ card G) = card ↑(S ^ card G * S ^ card G)

Tactic:
← pow_add,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ card ↑(S ^ card G) = card ↑(S ^ (card G + card G))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| = 1
⊢ orderOf x ≤ 2

Tactic:
rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)

Goal state after:
case inr.inl
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2

case inr.inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ n • 1 = 0 ↔ addOrderOf 1 ∣ n

Tactic:
addOrderOf_dvd_iff_nsmul_eq_zero

Goal state after:
R : Type u_6
inst✝ : NonAssocRing R
n : ℕ
⊢ n • 1 = 0 ↔ n • 1 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
notMem_support_iff.1 hn

Goal state after:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then 0 else 0) = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + n + 1) ∣ p * (X - C a) ^ n

Tactic:
add_assoc,

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + (n + 1)) ∣ p * (X - C a) ^ n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X) = C a

Tactic:
simp [C_mul_X_eq_monomial, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p (a * (expand R p) f) + contract p (b * (expand R p) g) = 1

Tactic:
← contract_add hp,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p (a * (expand R p) f + b * (expand R p) g) = 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (C ↑n) = 0

Tactic:
exact derivative_C

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
have := degree_add_divByMonic hg hgf

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree