mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf (a • 1) = n / n.gcd a

Tactic:
addOrderOf_nsmul' _ a0,

Goal state after:
a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf 1 / (addOrderOf 1).gcd a = n / n.gcd a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

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 + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑(Fin.cast h (a + b)) = ↑(Fin.cast h a + Fin.cast h b)

Tactic:
rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (0 - 1).cast = ↑n - 1

Tactic:
zero_sub,

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (-1).cast = ↑n - 1
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
mul_comm,

Goal state after:
n : ℕ
x : ℕ × ℕ
⊢ x.swap.2 * x.swap.1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
mul_comm,

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ ↑m * ↑(↑m)⁻¹.val = 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
mul_comm,

Goal state after:
m n✝ n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u).val.Coprime n

Tactic:
rcases n with - | n
  · rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp
  apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
  have := Units.ext_iff.1 (mul_inv_cancel u)
  rw [Units.val_one] at this
  rw [← natCast_eq_natCast_iff, Nat.cast_one, ← this]; clear this
  rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
  rw [Units.val_mul, val_mul, natCast_mod]

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

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1

Tactic:
mul_comm,

Goal state after:
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : 1 * b = a * 1
⊢ a = b

Tactic:
one_mul,

Goal state after:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : b = a * 1
⊢ a = b
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ b * ∑ i ∈ range n.succ, a / b ^ i - 1 * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
mul_comm,

Goal state after:
a b n : ℕ
⊢ (∑ i ∈ range n.succ, a / b ^ i) * b - 1 * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ ∑ i ∈ range n.succ, a / b ^ i * b - 1 * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
one_mul,

Goal state after:
a b n : ℕ
⊢ ∑ i ∈ range n.succ, a / b ^ i * b - ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)

Tactic:
calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

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

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ a ≠ -a

Tactic:
by
  rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val + (n - b.val)) % n = a.val - b.val

Tactic:
← Nat.add_sub_assoc (le_of_lt (val_lt _)),

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val + n - b.val) % n = a.val - b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a.cast.cast = a

Tactic:
cast_eq_val,

Goal state after:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ ↑a.cast.val = a
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ (a + (l + 1)) ∣ p ^ a * b
⊢ False

Tactic:
Nat.pow_add,

Goal state after:
case inl
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ a * p ^ (l + 1) ∣ p ^ a * b
⊢ False
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

Tactic:
Nat.pow_add,

Goal state after:
case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by
  exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_natCast] at hn'

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn₀; · simp
  rcases eq_or_ne p 1 with rfl | hp₁; · simp
  simpa [*] using pow_dvd_iff_le_padicValNat (k := 1) hp₁ hn₀ |>.symm |>.not

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ ¬FiniteMultiplicity p (a + b)

Tactic:
contrapose hm

Goal state after:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
mul_comm,

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n * n ^ k).factorization = (k + 1) • n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac * orderOf x ∣ orderOf x * a

Tactic:
mul_comm,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ orderOf x * a.minFac ∣ orderOf x * a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization p = ∑ x ∈ S, (g x).factorization p

Tactic:
rw [factorization_prod hS, finsetSum_apply]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_isUnit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp

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

Goal state before:
pp: d n : ℕ
h : d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
by
  rcases eq_or_ne d 0 with (rfl | hd); · simp [zero_dvd_iff.mp h]
  rcases eq_or_ne n 0 with (rfl | hn); · simp [tsub_eq_zero_of_le]
  apply add_left_injective d.factorization
  simp only
  rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
    Nat.div_mul_cancel h]

Goal state after:
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 * orderOf y ∣ 1 * orderOf y

Tactic:
one_mul,

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 * orderOf y ∣ orderOf y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ x ^ (i * ↑(orderOf x)) = 1

Tactic:
mul_comm,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ x ^ (↑(orderOf x) * i) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.primeFactors ∩ n.primeFactors).prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
mul_comm,

Goal state after:
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.primeFactors ∪ n.primeFactors).prod f * (m.primeFactors ∩ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ ↑(orderOf x) ∣ 0 - (m - n) ↔ ↑(orderOf x) ∣ n - m

Tactic:
zero_sub,

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ ↑(orderOf x) ∣ -(m - n) ↔ ↑(orderOf x) ∣ n - m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
by
  ext x
  simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]
  rintro h1 -
  exact iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
    (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card ↥(zpowers x) * card (G ⧸ zpowers x)

Tactic:
mul_comm,

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ 1 * (x /ᵒᶠ g).coeff d = x.coeff (g + d)

Tactic:
one_mul,

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (x /ᵒᶠ g).coeff d = x.coeff (g + d)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ _root_.Pairwise (Function.onFun Coprime fun p ↦ ↑p ^ n.factorization ↑p)

Tactic:
intro p1 p2 hp

Goal state after:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 p2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · grw [← Nat.primeFactors_pow k hn, Nat.primeFactors_mono h <| pow_ne_zero n hk]
  · grw [dvd_prod_primeFactors_pow_self hn, prod_dvd_prod_of_subset _ _ _ h, prod_primeFactors_dvd]

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✝² : 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

Tactic:
one_mul,

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 = (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 * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
one_mul,

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 = (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
⊢ Finset.image (fun i ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
let : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x) := (zpowers x).instFintypeSubtypeMemOfDecidablePred
⊢ Finset.image (fun i ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
⊢ p.degree = m

Tactic:
· obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh
    exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (X ^ p) ^ q = r • X ^ (q * p)

Tactic:
mul_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (X ^ p) ^ q = r • X ^ (p * q)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (p * n) = f.coeff n

Tactic:
mul_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (n * p) = f.coeff n
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
one_mul,

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p) * g.coeff x.2 = ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
coeff_contract hp

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2

Tactic:
mul_comm,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ p * ((x, y).1 + (x, y).2) = (p * x, p * y).1 + (p * x, p * y).2
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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 : ℕ
⊢ (if p ∣ n then (contract p f).coeff (n / p) else 0) = f.coeff n

Tactic:
coeff_contract hp

Goal state after:
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 : ℕ
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ 1 * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
one_mul,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ (p /ₘ q).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: 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 : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((X - C r) ^ (p ^ n * rootMultiplicity (r ^ p ^ n) f) * (expand R (p ^ n)) g)

Tactic:
mul_comm,

Goal state after:
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 : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) g * (X - C r) ^ (p ^ n * rootMultiplicity (r ^ p ^ n) f))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree

Tactic:
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)

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

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ 1 * p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i

Tactic:
one_mul,

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_6
s : ι → Set α
⊢ (⨅ i, 𝓟 (s i)).HasBasis (fun t ↦ t.Finite) fun t ↦ ⋂ i ∈ t, s i

Tactic:
refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩

Goal state after:
α : Type u_1
ι : Type u_6
s : ι → Set α
U : Set α
⊢ (∃ t, U ∈ ⨅ i ∈ t, 𝓟 (s i)) ↔ ∃ i, i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
⊢ (pi fun x ↦ f).HasBasis (fun Ik ↦ Ik.1.Finite ∧ p Ik.2) fun Ik ↦ Ik.1.pi fun x ↦ s Ik.2

Tactic:
refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)

Goal state after:
ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
I : Set ι
k : ι → κ
hI : I.Finite
hk : ∀ i ∈ I, p (k i)
⊢ ∃ k₀, p k₀ ∧ ∀ i ∈ I, s k₀ ⊆ s (k i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = C q.leadingCoeff * p

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p * C q.leadingCoeff
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = map Prod.swap (g ×ˢ f)

Tactic:
rw [prod_comm', ← map_swap_eq_comap_swap]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
by
  simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]; ac_rfl

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

Goal state before:
pp: case mp
α : Type u_2
f : Filter α
⊢ f.ker = ∅ → f.kerᶜ ∈ f

Tactic:
intro h
    simp [h]

Goal state after:
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r * GCDMonoid.gcd p q / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r * GCDMonoid.gcd p q / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s : σ
f : σ →₀ R
⊢ (weight (Pi.single s 1)) f = f s

Tactic:
by
  rw [weight_single_index, smul_eq_mul, mul_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = (p * C ((↑u).coeff 0)).roots

Tactic:
mul_comm,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = (C ((↑u).coeff 0) * p).roots