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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Tactic:
refine ⟨x, hx, ?_⟩

Goal state after:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ↑(f b).natDegree ≤ (f x).degree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ (C b * p).Monic

Tactic:
unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (p * C b).Monic

Tactic:
unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

Goal state before:
pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
refine C_mul_pow _ _ ?_ df

Goal state after:
case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
rwa [leadingCoeff_monic_mul hp]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0

Tactic:
conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
  constructor
  · intro h
    rw [h, zero_mul]
  · intro h
    rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (j 0) j.tail
⊢ False

Tactic:
rw [cons_tail] at hjmi

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hadd
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree

Tactic:
· exact natDegree_add_le

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
have := (Commute.one_right x).geom_sum₂_mul_add n
  rw [one_pow, geom_sum₂_with_one] at this
  exact this

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
have hincl : of' R M '' f.coeff.support ⊆ ⋃ g ∈ S, of' R M '' g.coeff.support :=
    fun s hs ↦ Set.mem_iUnion₂.2 ⟨f, hf, hs⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S

Tactic:
have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
    simp only [hS, top_toSubmodule, Submodule.mem_top]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R R[M] ↔ AddMonoid.FG M

Tactic:
by
  refine ⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
  obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
  refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩
  have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
    simp only [hS, top_toSubmodule, Submodule.mem_top]
  rw [adjoin_eq_span] at hm
  exact mem_closure_of_mem_span_closure hm

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

Tactic:
exact (this R p h.symm (le_of_not_ge hle)).symm

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

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℕ
ha : ↑a < ↑p
b : ℕ
hb : ↑b < ↑p
hab : ↑↑a = ↑↑b
⊢ ↑a = ↑b

Tactic:
norm_cast at *

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : ↑a = ↑b
⊢ a = b
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
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
y : R
hy : y ∈ ker f ∧ (Quotient.mk I) y = x
⊢ x ∈ ker (Quotient.lift I f H)

Tactic:
rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]

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
y : R
hy : y ∈ ker f ∧ (Quotient.mk I) y = x
⊢ f y = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : r • 1 ∈ s
⊢ False

Tactic:
exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

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

Goal state before:
pp: case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
exact isPeriodicPt_zero f x

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

Tactic:
rw [← Nat.card_prod, Nat.card_congr]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↥s × ↑(QuotientGroup.mk '' t)
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : StarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S

Tactic:
cases S; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

Tactic:
cases S; rfl

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ ¬s.permutations.Nodup

Tactic:
duplicate_iff_sublist

Goal state after:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
⊢ ¬s.permutations.Nodup
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

Tactic:
intro hyp

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
⊢ ∀ g ∈ H, g • s ⊆ s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

Tactic:
intro hyp

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
rw [← val_intCast, val]; rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index = Nat.card ↥f.ker

Tactic:
rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Tactic:
· rintro ⟨rfl, hn⟩
    exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

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

Goal state before:
pp: case case1
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
| case1 p hp hmod e q heq hqp ih =>

Goal state after:
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
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length

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 ∈ {tl.length}, ofDigits p (List.drop x tl) = ofDigits p (List.drop tl.length tl)
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

Tactic:
← ofDigits_digits b' n

Goal state after:
case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits b' (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

Tactic:
← ofDigits_digits b' n

Goal state after:
case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑(ofDigits b' (b'.digits n))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder a → IsOfFinOrder (a ^ n)

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨m, hm, ha⟩
  exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Tactic:
unfold FiniteMultiplicity
  congr! 3
  simp only [dvd_neg]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
minimalPeriod_eq_one_iff_isFixedPt,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ IsFixedPt (fun x_1 ↦ x * x_1) 1 ↔ x = 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (n.factorization p + 1) ∣ n
⊢ False

Tactic:
← factorization_le_iff_dvd (pow_ne_zero _ hp.ne_zero) hn

Goal state after:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False
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
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
fixedLengthDigits_succ_eq_disjiUnion,

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
⊢ ∑ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯, L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ n !.factorization p - (k ! * (n - k)!).factorization p = 0

Tactic:
factorization_factorial_eq_zero_of_lt h,

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

Tactic:
Ico_add_one_right_eq_Icc

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ m ∈ Icc 0 (p ^ n), x ^ m * y ^ (p ^ n - m) * ↑((p ^ n).choose m) =
    ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ (k + m) = x ^ (m + k)

Tactic:
by simp [Nat.add_comm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ Nat.card G

Tactic:
simpa using orderOf_le_card_univ

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
u : Gˣ
⊢ IsOfFinOrder u

Tactic:
apply isOfFinOrder_of_finite

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ 0 < card R

Tactic:
Fintype.card_pos_iff

Goal state after:
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ Nonempty R
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hn : n ≠ 0
⊢ g ≠ 0

Tactic:
· exact gcd_ne_zero_right hn

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ df + dg ≠ d

Tactic:
exact ne_comm.mp h

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m

pp: case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0

Tactic:
· subst h h_pow_bas
    exact coeff_pow_of_natDegree_le ‹_›

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
hq,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * 0).trailingDegree = p.trailingDegree + trailingDegree 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun a b ↦ b * ↑a * if n = a - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
rw [sum, Finset.sum_eq_single (n + 1)]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ (aeval r) ((expand R p) P) = (aeval (r ^ p)) P

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
  rw [map_add, aeval_add, aeval_add, hf, hg]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p /ₘ 0 = 0

Tactic:
unfold divByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f + g) = contract p f + contract p g

Tactic:
by
  ext; simp_rw [coeff_add, coeff_contract hp, coeff_add]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative (C (p.coeff 0)) = 0

Tactic:
derivative_C

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p /ₘ q = 0

Tactic:
unfold divByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
unfold divByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).1
      else 0).degree ≤
    p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ coeff 0 n = 0

case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.degree < (X - C a).degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ (⇑derivative)^[i] p ≠ 0 → i ∈ range (p.natDegree + 1)

Tactic:
contrapose; simp_all [iterate_derivative_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
⊢ False

Tactic:
hq,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * ((X - C a) * q) = p
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree = 0
⊢ derivative (C (p.coeff 0)) = 0

Tactic:
derivative_C

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree = 0
⊢ 0 = 0
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
h : ∃ x, f = ⨅ i, 𝓟 (x i)
⊢ f.IsCountablyGenerated

Tactic:
rcases h with ⟨x, rfl⟩

Goal state after:
α : Type u_1
x : ℕ → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Tactic:
exact ⟨p.natTrailingDegree,
      fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt_add_one _⟩

Goal state after: