mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H.subgroupOf ⊥).index = 1

Tactic:
subgroupOf_bot_eq_top,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊤.index = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : H.IsFiniteRelIndex L
h : H ≤ K
⊢ K.IsFiniteRelIndex L

Tactic:
rw [isFiniteRelIndex_iff_finiteIndex] at *
  exact finiteIndex_of_le <| subgroupOf_mono L h

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

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

Tactic:
split_ifs with hk

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

case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
split_ifs with hk
  · rw [hk, zero_sub, ZMod.cast_neg_one]
  · cases n
    · dsimp [ZMod, ZMod.cast]
      rw [Int.cast_sub, Int.cast_one]
    · dsimp [ZMod, ZMod.cast, ZMod.val]
      rw [Fin.coe_sub_one, if_neg]
      · rw [Nat.cast_sub, Nat.cast_one]
        rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
      · exact hk

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
· grw [← hx]
      gcongr
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
rintro ⟨k, hk, rfl⟩

Goal state after:
case refine_2
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
rw [← add_le_add_iff_left a]

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

Tactic:
obtain (_ | _ | n) := n
    · simpa [ZMod] using not_subsingleton _
    · simp [ZMod]
    · simpa [ZMod] using not_subsingleton _

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

Goal state before:
pp: n : ℕ
⊢ n.centralBinom ≤ 4 ^ n

Tactic:
by
  grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]

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

Goal state before:
pp: case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

Tactic:
clear IH; exact False.elim ((not_lt.2 n_big) hn)

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

Goal state before:
pp: case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

Tactic:
norm_num [centralBinom, choose]

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

Goal state before:
pp: n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * (2 * n + 1) * n.centralBinom

Tactic:
← succ_mul_centralBinom_succ,

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ (n + 1) * (n + 1).centralBinom
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h : L ≠ []
⊢ L.getLast h ≠ 0

Tactic:
rw [List.getLast_cons h] at w₂

Goal state after:
case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
h : L ≠ []
w₂ : L.getLast h ≠ 0
⊢ L.getLast h ≠ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
⊢ n.divMaxPow p * p ^ padicValNat p n = n

Tactic:
by
  unfold divMaxPow padicValNat
  fun_cases maxPowDvdDiv with
  | case1 h => exact go_spec h |>.1
  | case2 h => simp

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

Goal state before:
pp: case e'_2.h
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

pp: case e'_2.a
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

pp: case e'_3
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
· refine (length_digits p n h hn).symm

Goal state after:
case e'_2.a
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

case e'_3
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

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

Goal state before:
pp: case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
if pp : p.Prime then ?_ else
    rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
    simp [factorization, pp]

Goal state after:
case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = n.factorization p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a + b

Tactic:
apply dvd_add
    · apply pow_dvd_of_le_emultiplicity
      exact h.le
    · simp

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

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization = f

Tactic:
Finsupp.prod,

Goal state after:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (∏ a ∈ f.support, a ^ f a).factorization = f
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList

Tactic:
intro q hq

Goal state after:
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList
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✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x * x ^ (orderOf x - 1) = 1

Tactic:
← _root_.pow_succ',

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ (orderOf x - 1 + 1) = 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ i ∈ Ico 1 (multiplicity m n + 1) ↔ i ∈ {i ∈ Ico 1 b | m ^ i ∣ n}

Tactic:
simp only [mem_Ico, Nat.lt_succ_iff,
              fin.pow_dvd_iff_le_multiplicity, mem_filter,
              and_assoc, and_congr_right_iff, iff_and_self]

Goal state after:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ 1 ≤ i → i ≤ multiplicity m n → i < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
⊢ IsMulTorsionFree G

Tactic:
by
    refine ⟨fun n hn a b hab ↦ ?_⟩
    rw [← div_eq_one] at hab ⊢
    simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG
    exact of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
obtain ⟨⟩ := nonempty_fintype G
  simpa using orderOf_le_card_univ

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

Goal state before:
pp: case zero
p : ℕ
⊢ #({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p

Tactic:
simp [Nat.succ_div, add_ite, ← insert_Ioc_right_eq_Ioc_add_one, filter_insert,
    apply_ite card, *]

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

Goal state before:
pp: case succ
p n✝ : ℕ
a✝ : #({x ∈ Ioc 0 n✝ | p ∣ x}) = n✝ / p
⊢ #({x ∈ Ioc 0 (n✝ + 1) | p ∣ x}) = (n✝ + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, ← insert_Ioc_right_eq_Ioc_add_one, filter_insert,
    apply_ite card, *]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ (g * g ^ (Nat.card G - 1)) • a
⊢ g • a = a

Tactic:
← _root_.pow_succ',

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g ^ (Nat.card G - 1 + 1) • a
⊢ g • a = a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : (g * g ^ (Nat.card G - 1)) • a ≤ g • a
⊢ g • a = a

Tactic:
← _root_.pow_succ',

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g ^ (Nat.card G - 1 + 1) • a ≤ g • a
⊢ g • a = a
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
h : p.coeff 0 = 0
⊢ False

Tactic:
simp [h] at h0'

Goal state after:
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✝ : R[X]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
sum_smul_index

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ (p.sum fun n a_1 ↦ C (a * a_1 * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
by
      have := Nontrivial.of_polynomial_ne hp0
      rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
      exact WithBot.bot_lt_coe _

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (⇑derivative)^[0] (p * q) = ∑ k ∈ range (Nat.succ 0), Nat.choose 0 k • ((⇑derivative)^[0 - k] p * (⇑derivative)^[k] q)

Tactic:
simp [Finset.range]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ ∀ (t : Set α), t ∈ ⨅ i, l i ↔ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
intro t
    constructor
    · simp only [mem_iInf', (hl _).mem_iff]
      rintro ⟨I, hI, V, hV, -, rfl, -⟩
      choose u hu using hV
      exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩
    · rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
      grw [← hsub]
      exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
rcases le_or_gt k m with hkm | hkm

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
l₁ l₂ : Filter α
⊢ (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Tactic:
simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f

Tactic:
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
  refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
  · rintro ⟨v, v_in, hv⟩ a a_in b b_in
    exact hv (mk_mem_prod a_in <| v_in b_in)
  · rintro ⟨x, y⟩ ⟨hx, hy⟩
    exact h hx y hy

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
⊢ i ∈ Iᶜ → f i '' I.piecewise (fun i ↦ id (s i)) (fun x ↦ univ) i = univ

Tactic:
(hiI : i ∉ I)

Goal state after:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
hiI : i ∉ I
⊢ f i '' I.piecewise (fun i ↦ id (s i)) (fun x ↦ univ) i = univ
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Tactic:
by
  simp only [Filter.coprod, mem_sup, compl_mem_comap]

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ derivative (Multiset.map f (i ::ₘ s)).prod =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) (i ::ₘ s)).sum

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s,
    Multiset.sum_cons, Multiset.erase_cons_head, mul_comm (derivative (f i))]

Goal state after:
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ↑k ! * derivative (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)) =
    ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
derivative_sum,

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑(k + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e_a
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q

Tactic:
rw [← Multiset.rel_eq, Multiset.rel_map]
  simp only [mk_eq_mk_iff_associated]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Tactic:
have h : (normalize : α → α) = Associates.out ∘ Associates.mk := by
    ext
    rw [Function.comp_apply, Associates.out_mk]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case refine_2
σ : Type u_1
a : σ
hp : ((single a 1).sum fun a k ↦ k) = 1
⊢ single a 1 ∈ Set.range fun a ↦ single a 1

Tactic:
use a

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ.zero
σ : Type u_5
s : Set ℕ
hn : 0 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((0 + 1) • s) = (0 + 1) • ⇑degree ⁻¹' s

Tactic:
simp_all [succ_nsmul, degree_preimage_add]

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ.succ
σ : Type u_5
s : Set ℕ
n✝ : ℕ
a✝ : n✝ + 1 ≠ 0 → ⇑degree ⁻¹' ((n✝ + 1) • s) = (n✝ + 1) • ⇑degree ⁻¹' s
hn : n✝ + 1 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n✝ + 1 + 1) • s) = (n✝ + 1 + 1) • ⇑degree ⁻¹' s

Tactic:
simp_all [succ_nsmul, degree_preimage_add]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x

Tactic:
· intro h
    obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h
    exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

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

Goal state before:
pp: case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0
⊢ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
use a

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬g.IsRoot t
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(C ↑m * g).IsRoot t

Tactic:
IsRoot

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬eval t (C ↑m * g) = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
⊢ p.primPart.natDegree = p.natDegree

Tactic:
by_cases h : C p.content = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
⊢ p.primPart.natDegree = p.natDegree