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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
· simp [hp1]

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)

Tactic:
by
  intro h
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp at h
  apply hn
  rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

Goal state after:
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 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)

Tactic:
simp only [this]

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

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ span (↥(adjoin R s)) (_root_.id '' q)
⊢ r ∈ span R (p * q)

Tactic:
Finsupp.mem_span_image_iff_linearCombination (adjoin R s)

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr :
  ∃ l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q, (Finsupp.linearCombination (↥(adjoin R s)) _root_.id) l = r
⊢ r ∈ span R (p * q)
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 : Subalgebra R A
h : S.FG
⊢ (map S.val ⊤).FG

Tactic:
rw [Algebra.map_top, range_val]

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (∅.prod f).coeff k ∈ I ^ (0 - k)

Tactic:
prod_empty,

Goal state after:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ coeff 1 k ∈ I ^ (0 - k)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P ↔ x ∈ comap C (map C P)

Tactic:
simp only [mem_comap, mem_map_C_iff]

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P ↔ ∀ (n : ℕ), (C x).coeff n ∈ P
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ f.FiniteType

Tactic:
by
  rw [← f.comp_id]
  exact (id A).comp_surjective hf

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

Goal state before:
pp: case inl
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a

Tactic:
exact mul_one _

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
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
x y : A
hx : star x ∈ S
hy : star y ∈ S
⊢ star (x * y) ∈ S

Tactic:
exact (star_mul x y).symm ▸ mul_mem hy hx

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

Goal state before:
pp: case cons.mp
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

pp: case cons.mpr
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
· rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
    · exact ⟨[], y :: ys, by simp⟩
    · exact ⟨y :: l₁, l₂, l0, by simp⟩

Goal state after:
case cons.mpr
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ⟨gv, gp⟩ • b✝ ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝

Tactic:
refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ ↑gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.length ≤ 1

Tactic:
induction s using Quotient.inductionOn'

Goal state after:
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ (comap K.subtype (comap f H)).index = H.relIndex (map f K)

Tactic:
comap_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ (map H.subtype K).index = K.index * H.index

Tactic:
rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ ↑a.cast = a

Tactic:
cases n
  · simp [ZMod.cast, ZMod]
  · dsimp [ZMod.cast]
    rw [Int.cast_natCast, natCast_zmod_val]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R) ∧ True

Tactic:
and_true

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val

Tactic:
apply Nat.mod_eq_of_lt h

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

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

Tactic:
rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ cons n n.properDivisors ⋯, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
Finset.sum_cons,

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ n + ∑ x ∈ n.properDivisors, x = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
← cons_self_properDivisors h.ne_zero,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ cons p p.properDivisors ⋯, f x = f p * f 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
Nat.mem_divisorsAntidiagonal

Goal state after:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + k + 1 - k) ^ k

Tactic:
Nat.add_right_comm,

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1 + k - k) ^ k
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 | ind n h => ?_
      cases n
      · rw [digits_zero]
        rfl
      · simp only [digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b ≤ ↑n
⊢ multiplicity a b ≤ n

Tactic:
by
  exact_mod_cast multiplicity_le_emultiplicity.trans h

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : emultiplicity a b < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
unfold emultiplicity at hm
  split at hm
  · simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)
  · simp at hm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑k

Tactic:
simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
    Decidable.not_not, true_and]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ ∀ n < k, a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
· apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp

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

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length + (replicate (l - (b.digits n).length) 0).length = l

Tactic:
length_replicate,

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length + (l - (b.digits n).length) = l
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Tactic:
rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt,
    Nat.le_zero]
  exact
    ⟨fun h =>
      or_iff_not_imp_right.2 fun hb =>
        have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
        Classical.by_contradiction fun ha1 : a ≠ 1 =>
          have ha_gt_one : 1 < a :=
            lt_of_not_ge fun _ =>
              match a with
              | 0 => ha rfl
              | 1 => ha1 rfl
              | b+2 => by lia
          not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
      fun h => by cases h <;> simp [*]⟩

Goal state after:
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 ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯, L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
Finset.sum_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
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
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:
by
              rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
              simp_all [mul_comm, mul_left_comm, pow_add]

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

Goal state before:
pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
α : Type u_6
inst✝ : MulAction G α
hx : x ∈ zpowers y
a : α
hs : y • a = a
⊢ x • a = a

Tactic:
by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
  rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, map_zpow _ y k,
    MulAction.toPermHom_apply]
  exact Function.IsFixedPt.perm_zpow (by exact hs) k

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ (fun x_1 ↦ x ^ x_1) (i % ↑(orderOf x)).natAbs = y

Tactic:
by
    dsimp only
    rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]

Goal state after:
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
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x

Tactic:
exact (isOfFinOrder_of_finite x).orderOf_pos

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G) = a ^ n

Tactic:
by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ False

Tactic:
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
⊢ False
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = rootMultiplicity a (C 1) + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
rootMultiplicity_C,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = 0 + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'

Goal state after:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : p ∣ n.succ
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f✝ : ι → Filter α
inst✝ : ∀ (i : ι), (f✝ i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f✝ i).HasAntitoneBasis (s i)
I : Set (PLift ι)
f : ↑I → ℕ
hI : ⟨I, f⟩.fst.Finite
⊢ ⟨I, f⟩ ∈ range (Sigma.map SetLike.coe fun x ↦ id)

Tactic:
lift I to Finset (PLift ι) using hI

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f✝ : ι → Filter α
inst✝ : ∀ (i : ι), (f✝ i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f✝ i).HasAntitoneBasis (s i)
I : Finset (PLift ι)
f : ↑↑I → ℕ
⊢ ⟨↑I, f⟩ ∈ range (Sigma.map SetLike.coe fun x ↦ id)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case h
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun t ↦ ⨅ i ∈ t, f i

Tactic:
exact directed_of_isDirected_le fun _ _ => biInf_mono

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.fst (comap Prod.fst f)) ⊓
        comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.fst (comap Prod.snd g)) ⊓
      comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.snd h) =
    comap Prod.fst f ⊓ (comap Prod.snd (comap Prod.fst g) ⊓ comap Prod.snd (comap Prod.snd h))

Tactic:
comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ ⇑(Equiv.prodAssoc α β γ).symm) g ⊓
      comap (Prod.snd ∘ ⇑(Equiv.prodAssoc α β γ).symm) h =
    comap Prod.fst f ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) h)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ l.kerᶜ.Countable

Tactic:
simp only [hs.ker, iInter_true, compl_iInter]

Goal state after:
α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ (⋃ i, (s i)ᶜ).Countable
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.fst f) ⊓
      (comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.snd (comap Prod.fst g)) ⊓
        comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.snd (comap Prod.snd h))) =
    comap Prod.fst (comap Prod.fst f) ⊓ comap Prod.fst (comap Prod.snd g) ⊓ comap Prod.snd h

Tactic:
comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (Prod.fst ∘ ⇑(Equiv.prodAssoc α β γ)) f ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) g ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ ⇑(Equiv.prodAssoc α β γ)) h) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) g ⊓ comap Prod.snd h
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ (Multiset.map Associates.mk (Multiset.map f p.val)).prod = Associates.mk (∏ i ∈ p, f i)

Tactic:
prod_mk,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ Associates.mk (Multiset.map f p.val).prod = Associates.mk (∏ i ∈ p, f i)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q

Tactic:
convert!
    normalize_eq_normalize hdvd
      ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
        (prime_of_normalized_factor _ hq).irreducible hdvd)

Goal state after:
case e'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = normalize p

case e'_3
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ q = normalize q
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
s : Set ℕ
n : ℕ
hn : n ≠ 0
⊢ ⇑degree ⁻¹' (n • s) = n • ⇑degree ⁻¹' s

Tactic:
obtain (_ | n) := n

Goal state after:
case zero
σ : Type u_5
s : Set ℕ
hn : 0 ≠ 0
⊢ ⇑degree ⁻¹' (0 • s) = 0 • ⇑degree ⁻¹' s

case succ
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n + 1) • s) = (n + 1) • ⇑degree ⁻¹' s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ normalizedFactors m.prod = m

pp: case inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m

Tactic:
· obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx
    simp

Goal state after:
case inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m