mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
rw [nodup_map_iff]

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])

pp: case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
· simp at hx

Goal state after:
case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))
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
hyp : H ≤ stabilizer G s
g : G
⊢ g ∈ H → g • s ⊆ s

Tactic:
hg

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 : G
hg : 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
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
⊢ g ∈ H → g ∈ stabilizer G s

Tactic:
hg

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
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a

Tactic:
by
  rw [chain_coe_cons, nil_append, List.isChain_pair]

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

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

Tactic:
hg

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ H.relIndex K * K.index = H.index

Tactic:
by
  rw [mul_comm]
  simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H

Tactic:
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]

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'
K : Subgroup G
f : G →* G'
⊢ f.ker.relIndex K = Nat.card ↥(map f K)

Tactic:
rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]

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

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m = n
⊢ ZMod m ≃+* ZMod n

Tactic:
rcases m with - | m <;> rcases n with - | n
  · exact RingEquiv.refl _
  · exfalso
    exact n.succ_ne_zero h.symm
  · exfalso
    exact m.succ_ne_zero h
  · exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h] }

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
have : Std.Asymm (α := ℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
  refine List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_
  simp [List.reverse_perm', List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList
    (nodup_divisorsAntidiagonalList.map Prod.swap_injective), mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors ⊆ Ico 1 (n + 1)

Tactic:
simp only [divisors, filter_subset]

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

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

pp: case inr
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
· constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases y
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

Goal state after:
case inr
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)

Tactic:
by
  simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
  rintro n han _ha hn hbn _hb -
  exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by
    simp +contextual [s, disjoint_left, Eq.comm, forall_comm (β := _ = _)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
by_cases h : a = 0

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case2
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, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd

Tactic:
rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]

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

Goal state before:
pp: case ind.succ.head
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2

Tactic:
exact n.succ.mod_lt (by linarith)

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

Goal state before:
pp: case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))

Tactic:
· assumption

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
rw [multiplicity_eq_of_emultiplicity_eq_some hm]

Goal state after:
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.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ ¬(a ≠ 1 ∧ 0 < b)

Tactic:
not_and_or,

Goal state after:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ ¬a ≠ 1 ∨ ¬0 < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) 1

Tactic:
by simpa using han

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
⊢ emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← Associates.mk_pow, Associates.mk_dvd_mk]

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_and_or,

Goal state after:
n p : ℕ
⊢ ¬Prime p ∨ ¬p ∣ n ∨ ¬n ≠ 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
add_tsub_cancel_right,

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
⊢ ↑(fixedLengthDigits hb l).card * (b * (b - 1) / 2) + ↑b * (l * b ^ (l - 1) * b.choose 2) =
    (l + 1) * b ^ l * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)

Tactic:
simpa [has, ← ih] using emultiplicity_mul hp

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

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
⊢ n.factorization p ≤ b

Tactic:
if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
⊢ orderOf (y ^ m) = orderOf y

Tactic:
by_cases hg : IsOfFinOrder y

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ n !.factorization p ≤ n / (p - 1)

Tactic:
rw [factorization_factorial hp (Nat.lt_add_one (log p n))]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: k x p : ℕ
hp : Prime p
hx : p ^ k ∣ x
⊢ x / p ^ k / p ^ (x / p ^ k).factorization p = x / p ^ x.factorization p

Tactic:
by
  obtain ⟨m, rfl⟩ := hx
  rw [Nat.mul_div_cancel_left m (pow_pos hp.pos k), ← ordCompl_self_pow_mul m k hp]

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
⊢ ↑(∑ i ∈ range n, p ^ i) + ↑(p ^ n) = ↑(∑ i ∈ range (n + 1), p ^ i)

Tactic:
Finset.sum_range_succ,

Goal state after:
case succ
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
⊢ ↑(∑ i ∈ range n, p ^ i) + ↑(p ^ n) = ↑(∑ x ∈ range n, p ^ x + p ^ n)
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
one_zpow,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 * (g ^ n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
one_zpow,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1

Tactic:
exact natDegree_C_mul_X_pow (n - 1) c c0

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
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ S ^ card G * S ^ card G = S ^ card G

Tactic:
classical
    apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
    simp_rw [← pow_add,
        Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : (X - C c).comp (C ⅟a * (X - C b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p

Tactic:
refine (pow_dvd_pow_of_dvd ((isUnit_C.mpr ha).dvd_mul_left.mp (dvd_of_eq ?_)) _).trans h

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : (X - C c).comp (C ⅟a * (X - C b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
⊢ X - C (a * c + b) = C a * (X - C c).comp (C ⅟a * (X - C b))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval (r ^ p) f + eval r ((expand R p) g) = eval (r ^ p) f + eval (r ^ p) g

Tactic:
hg

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval (r ^ p) f + eval (r ^ p) g = eval (r ^ p) f + eval (r ^ p) g
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (p %ₘ q).degree < q.degree

Tactic:
by
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h]
          exact lt_of_not_ge

Goal state after:
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
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval (r ^ p)) f + (aeval r) ((expand R p) g) = (aeval (r ^ p)) f + (aeval (r ^ p)) g

Tactic:
hg

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval (r ^ p)) f + (aeval (r ^ p)) g = (aeval (r ^ p)) f + (aeval (r ^ p)) g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial (n + 1 - 1)) (a * ↑(n + 1)) = (monomial n) (a * (↑n + 1))

Tactic:
add_tsub_cancel_right,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial n) (a * ↑(n + 1)) = (monomial n) (a * (↑n + 1))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
convert! prime_X_sub_C (0 : R)
  simp

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

Goal state before:
pp: S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

Tactic:
by_contra! ⟨hp, hq⟩
  rcases h with ⟨_, _, h⟩
  apply_fun aeval s at h
  simp only [map_add, map_mul, map_one, hp, hq, mul_zero, add_zero, zero_ne_one] at h

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬X - C (r ^ p ^ n) ∣ g
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Tactic:
conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n m : ℕ
c : R
hm : m ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (f ^ n))

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m.succ] (f ^ n))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ i, f i
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
rw [← iInf_range' (g := (·))] at hs

Goal state after:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
by
  have := hs.to_subtype
  rw [biInter_eq_iInter, biInter_eq_iInter]
  exact .iInter fun i ↦ hle i.1 i.2

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ update f a b =ᶠ[𝓟 {a}ᶜ] f

Tactic:
by
  filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
⊢ (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
hg

Goal state after:
case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
⊢ Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
⊢ (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Tactic:
hg

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
⊢ (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree

pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
· simp [hp0]

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
⊢ ℕ∞

Tactic:
by_cases h : a = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : a = 0
⊢ ℕ∞

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : ¬a = 0
⊢ ℕ∞