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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
s : Cycle α
hs : s.Nodup
⊢ ∃ a, (fun l ↦ ⟨↑↑l, ⋯⟩) a = ⟨s, hs⟩

Tactic:
induction s using Quotient.inductionOn' with

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
hs✝ : List α
hs : Nodup (Quotient.mk'' hs✝)
⊢ ∃ a, (fun l ↦ ⟨↑↑l, ⋯⟩) a = ⟨Quotient.mk'' hs✝, hs⟩
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k ≤ Nat.log 2 (p ^ k)

Tactic:
· calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

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

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
h : (orbitRel (↥H) X) y₁ y₂
⊢ ↑⋯.choose = ↑⋯.choose

Tactic:
rw [orbitRel_apply] at h

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ ↑⋯.choose = ↑⋯.choose
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:
K.index_map_of_injective H.subtype_injective,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ K.index * H.subtype.range.index = K.index * H.index
Module: Mathlib.Data.ZMod.Basic

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

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

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

Goal state before:
pp: case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑↑(a + b) = if ↑(n + 1) ≤ ↑↑a + ↑↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
simp only [Fin.val_add_eq_ite, Int.natCast_succ]

Goal state after:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if ↑n + 1 ≤ ↑↑a + ↑↑b then cast a + cast b - (↑n + 1) else cast a + cast b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast

Tactic:
rcases n with - | n
  · simp; rfl
  change Fin (n + 1) at a b
  change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _
  simp only [Fin.val_add_eq_ite, Int.natCast_succ]
  norm_cast
  split_ifs with h
  · rw [Nat.cast_sub h]
    congr
  · rfl

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n

Tactic:
rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
ext ⟨d, nd⟩
  simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
    Prod.ext_iff, and_left_comm, exists_eq_left]
  constructor
  · rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
    rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
    exact ⟨rfl, hn⟩
  · rintro ⟨rfl, hn⟩
    exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

Tactic:
cases n
  · rw [properDivisors_zero, subset_empty] at hsub
    simp [hsub]
  classical
    rw [← sum_sdiff hsub]
    intro h
    apply Subset.antisymm hsub
    rw [← sdiff_eq_empty_iff_subset]
    contrapose! h
    apply ne_of_lt
    rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
    gcongr
    have hlt :=
      sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
    simp only [sum_const_zero] at hlt
    apply hlt

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

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
rw [mul_assoc]; refine Nat.le_mul_of_pos_left _ zero_lt_two

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
⊢ (a - b).val = a.val - b.val

Tactic:
by_cases hb : b = 0
  · cases hb; simp
  · have : NeZero b := ⟨hb⟩
    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

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

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
| succ m ih =>

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ (m + 1)).val ≤ a.val ^ (m + 1)

Tactic:
| succ m ih =>

Goal state after:
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
⊢ ∀ l ∈ L, l < b

Tactic:
intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m

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

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

Tactic:
rw [h _ (Nat.div_lt_self' _ b)]

Goal state after:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)

Tactic:
rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ 0 < multiplicity a b

Tactic:
simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

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

Goal state before:
pp: case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
rcases eq_or_ne p 1 with rfl | hp₁

Goal state after:
case inr.inl
n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat 1 n = 0 ↔ 1 = 1 ∨ n = 0 ∨ ¬1 ∣ n

case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)

Tactic:
rw [emultiplicity_neg, Int.natCast_emultiplicity]

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

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ (d :: L).length = l + 1

pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
· simpa using ((mem_fixedLengthDigits_iff hb).mp hL).1

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
exact ((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

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

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization

Tactic:
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
hT : T.prod g ≠ 0
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).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
⊢ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]
    exact Exists.intro n (id ⟨hn, hx⟩)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n✝ m✝ : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
this : (n + k).choose k * k ! * n ! = (n + k)!
⊢ emultiplicity p ((n + k).choose k * k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]

Tactic:
by
  rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
apply map_natDegree_eq_sub (φ := divX_hom)
  · intro f
    simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero
  · intro n c c0
    rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]
    split_ifs with n0
    · simp [n0]
    · exact natDegree_C_mul_X_pow (n - 1) c c0

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

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases ha0 : a = 0

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
← Nat.mod_add_div n p,

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p + p * (n / p)) = 0
⊢ p ∣ n
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - 0) (p.comp (X + C t))

Tactic:
sub_zero

Goal state after:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity X (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).2 = p
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p = p
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ i, (i.Finite ∧ i ⊆ s) ∧ ⋂₀ i ⊆ U

Tactic:
by simp only [mem_generate_iff, and_assoc, and_left_comm]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - 0 = eval a p

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p = eval a p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = p %ₘ (X - 0)

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = p %ₘ X
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x p - 0 = eval₂ f x p

Tactic:
sub_zero

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x p = eval₂ f x p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
⊢ C (↑n + 1) * p ^ n * derivative p = C ↑n.succ * p ^ n * derivative p

Tactic:
n.cast_succ

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
⊢ C (↑n + 1) * p ^ n * derivative p = C (↑n + 1) * p ^ n * derivative p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂

Tactic:
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative)^[m + 1] p

Tactic:
| succ m ih =>

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑((n - k) * n.descFactorial k) * X ^ (n - (k + 1))

Tactic:
Nat.cast_mul

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(n.descFactorial k) * X ^ (n - (k + 1))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), ∃ t, (∀ (i_1 : p ↑i), s ↑i ⊆ t i_1) ∧ V i = ⋂ (i : p ↑i), t i) ∧ t = ⋂ i, V i) →
    ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Tactic:
rintro ⟨I, hIf, V, hV₁, hV₂, rfl⟩

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
hV₁ : ∀ (i : ↑I), ∃ t, (∀ (i_1 : p ↑i), s ↑i ⊆ t i_1) ∧ V i = ⋂ (i : p ↑i), t i
⊢ ∃ I_1, I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ ⋂ i ∈ I_1, s i ⊆ ⋂ i, V i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
· rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]

Goal state after:
case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (X - C a).degree ≤ p.degree

Tactic:
rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
x✝ : Set α
⊢ (∃ t₂ ∈ g, ∀ x ∈ x✝, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x | (fun y ↦ ∀ x ∈ x✝, (x, y) ∈ s) x}
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
  exact hnot_hnot_le

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
⊢ univ.pi s ∈ pi l

Tactic:
by
  filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _
  if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤

Tactic:
rintro ⟨b, rfl⟩
    exact hnot_boundary _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Tactic:
by
  rw [Tendsto, Prod.map_def, ← prod_map_map_eq]
  exact Filter.prod_mono hf hg

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ 1 - 0 = 1

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝ : Ring R
c : R
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
P : R[X]
h : P.degree < ↑0
⊢ (⇑derivative)^[0] P = 0

pp: case succ
R : Type u
inst✝ : CommRing R
n✝ : ℕ
a✝ : ∀ {P : R[X]}, P.degree < ↑n✝ → (⇑derivative)^[n✝] P = 0
P : R[X]
h : P.degree < ↑(n✝ + 1)
⊢ (⇑derivative)^[n✝ + 1] P = 0

Tactic:
case zero => exact degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
n✝ : ℕ
a✝ : ∀ {P : R[X]}, P.degree < ↑n✝ → (⇑derivative)^[n✝] P = 0
P : R[X]
h : P.degree < ↑(n✝ + 1)
⊢ (⇑derivative)^[n✝ + 1] P = 0
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c✝ ∈ {r | IsUnit r ∨ Prime r}

pp: case cons.inr.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
· right; exact ha₂

Goal state after:
case cons.inr.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False

Tactic:
rw [← one_smul R (w s)] at h
  apply zero_ne_one.symm (α := R)
  exact NonTorsionWeight.eq_zero_of_smul_eq_zero h

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
rw [normalizedFactors, factors, dif_neg ane0]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (Classical.choose ⋯)).prod ~ᵤ a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = (X - 0).roots

Tactic:
sub_zero

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = X.roots