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

Goal state before:
pp: case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))

Tactic:
← append_assoc,

Goal state after:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++
      map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ (y :: z :: zs).nextOr y d = (y :: z :: zs).nextOr y d'

Tactic:
nextOr_self_cons_cons,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ z = (y :: z :: zs).nextOr y d'
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x

Tactic:
by
  rw [Function.isPeriodicPt_iff_minimalPeriod_dvd, Nat.dvd_prime hp.out,
    ← minimalPeriod_eq_one_iff_isFixedPt.not, or_and_right, and_not_self_iff, false_or,
    iff_self_and]
  exact fun h ↦ ne_of_eq_of_ne h hp.out.ne_one

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : a = head
⊢ (head :: tail).prev a ha =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ (head :: tail).prev a ha =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]

Tactic:
· subst ha₀
    simp
    grind

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ (head :: tail).prev a ha =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ s.reverse.Nontrivial ↔ s.Nontrivial

Tactic:
simp [Nontrivial]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ¬(↑[]).Nontrivial

Tactic:
simp [Nontrivial]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ ¬(↑[x]).Nontrivial

Tactic:
simp [Nontrivial]

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

Goal state before:
pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
simp_rw [← prime_iff]
    exact fun p => prime_of_mem_primeFactorsList

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

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

Tactic:
rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]

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

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p

Tactic:
· rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]

Goal state after:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index

Tactic:
rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
exact cardinalMk_eq_max.le

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ 0 < x * ∑ i ∈ range n, x ^ i + 1 ∧ x * ∑ i ∈ range n, x ^ i + 1 < 1

Tactic:
add_lt_iff_neg_right,

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ 0 < x * ∑ i ∈ range n, x ^ i + 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a✝ : ℕ
⊢ a✝ ∈ image Prod.fst n.divisorsAntidiagonal ↔ a✝ ∈ n.divisors

Tactic:
simp [Dvd.dvd, @eq_comm _ n (_ * _)]

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
rw [← Nat.not_even_iff_odd] at h

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
val_mul,

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

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

Tactic:
by
      rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases y
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases x
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

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

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

Tactic:
exact ⟨left_inv, left_inv.rightInverse_of_card_le (by simp)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
ext; simp [mem_divisorsAntidiag, Prod.ext_iff, neg_eq_iff_eq_neg]

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

Goal state before:
pp: case inr.refine_1
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
⊢ l < b

Tactic:
rcases (List.mem_append.mp hl) with (h | h)

Goal state after:
case inr.refine_1.inl
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

case inr.refine_1.inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b
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:
| succ i hi =>

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

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

Tactic:
induction i with

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

Goal state before:
pp: p n : ℕ
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)
      · refine (length_digits p n h hn).symm
      all_goals exact (ofDigits_digits p n).symm
  · simp
  · simp [lt_one_iff.mp h]
    cases n
    all_goals simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
n : ℕ
⊢ multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
h hnx

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

Tactic:
rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
    exact List.replicate_sublist_iff.mpr le_rfl |>.subperm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs

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

Tactic:
· rw [Int.natCast_emultiplicity]

Goal state after:
case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
rcases Int.natAbs_eq b with h | h <;> conv_rhs => rw [h]
  · rw [Int.natCast_emultiplicity]
  · 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 : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
have hL₃ : L ≠ [] := by simp [ne_nil_iff_length_pos, hL₁]

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n.factorization n.minFac ≠ 0

Tactic:
refine mt (factorization_eq_zero_iff _ _).mp ?_

Goal state after:
n : ℕ
hn : 1 < n
⊢ ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr.inl
n p : ℕ
hp : Prime p
n_eq_zero : n = 0
⊢ n / p ^ n.factorization p = n

pp: case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n

Tactic:
· simp [n_eq_zero]

Goal state after:
case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d.factorization ≤ (n / p ^ n.factorization p).factorization

Tactic:
factorization_ordCompl

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d.factorization ≤ Finsupp.erase p n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ x ∈ ↑(Submonoid.closure s)

Tactic:
apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ x ∈ powers x⁻¹
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g ∧ 1 ≤ g
⊢ zpowers |g|ₘ = zpowers g

Tactic:
simp only [h, zpowers_inv]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g⁻¹ ∧ g < 1
⊢ zpowers |g|ₘ = zpowers g

Tactic:
simp only [h, zpowers_inv]

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

Goal state before:
pp: n p : ℕ
⊢ #({e ∈ Finset.range n | p ∣ e + 1}) = n / p

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
rintro p q (hp | hp) (hq | hq)
    · refine Or.inl ?_
      rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp
    · exact Or.inr (h_add hp hq)

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

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

Tactic:
exact bot_unique h_deg_le

Goal state after:
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
⊢ ¬(p /ₘ q).leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero

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 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : p.leadingCoeff = 0
⊢ False

Tactic:
leadingCoeff_eq_zero

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p

Tactic:
apply one_dvd

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p

Tactic:
rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]

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

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n] p * X + n • (⇑derivative)^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ, (n.choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n - k] p * X ^ (1 - k))

Tactic:
rcases n with rfl | n

Goal state after:
case e'_3.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0] p * X + 0 • (⇑derivative)^[0 - 1] p =
    ∑ k ∈ range (min 1 0).succ, (Nat.choose 0 k * Nat.descFactorial 1 k) • ((⇑derivative)^[0 - k] p * X ^ (1 - k))

case e'_3.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative)^[n + 1] p * X + (n + 1) • (⇑derivative)^[n + 1 - 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n + 1 - k] p * X ^ (1 - k))
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi t ⊆ eval i ⁻¹' s
⊢ s ∈ f i

Tactic:
← image_subset_iff

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n + 1] p * X + n • (⇑derivative)^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n - k] (derivative p) * X ^ (1 - k))

Tactic:
rcases n with rfl | n

Goal state after:
case e'_3.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 1] p * X + 0 • (⇑derivative)^[0] p =
    ∑ k ∈ range (min 1 0).succ,
      (Nat.choose 0 k * Nat.descFactorial 1 k) • ((⇑derivative)^[0 - k] (derivative p) * X ^ (1 - k))

case e'_3.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative)^[n + 1 + 1] p * X + (n + 1) • (⇑derivative)^[n + 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n + 1 - k] (derivative p) * X ^ (1 - k))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n + 2] p * X ^ 2 + (2 * n) • (⇑derivative)^[n + 1] p * X + (n * (n - 1)) • (⇑derivative)^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[n - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
rcases n with rfl | n

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 2] p * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] p * X + (0 * (0 - 1)) • (⇑derivative)^[0] p =
    ∑ k ∈ range (min 2 0).succ,
      (Nat.choose 0 k * Nat.descFactorial 2 k) • ((⇑derivative)^[0 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

case succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative)^[n + 1 + 2] p * X ^ 2 + (2 * (n + 1)) • (⇑derivative)^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative)^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[n + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative)^[n + 1 + 2] p * X ^ 2 + (2 * (n + 1)) • (⇑derivative)^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative)^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[n + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
rcases n with rfl | n

Goal state after:
case succ.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 1 + 2] p * X ^ 2 + (2 * (0 + 1)) • (⇑derivative)^[0 + 1 + 1] p * X +
      ((0 + 1) * (0 + 1 - 1)) • (⇑derivative)^[0 + 1] p =
    ∑ k ∈ range (min 2 (0 + 1)).succ,
      ((0 + 1).choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[0 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative)^[n + 1 + 1 + 2] p * X ^ 2 + (2 * (n + 1 + 1)) • (⇑derivative)^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative)^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative)^[n + 1 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ f.kerᶜ ∈ q.2

Tactic:
← disjoint_principal_left,

Goal state after:
case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Disjoint (𝓟 f.ker) q.2
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite

Tactic:
simp_rw [degree_eq_weight_one]
  refine finite_of_nat_weight_le (Function.const σ 1) ?_ n
  intro _
  simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map normalize (a ::ₘ 0)

Tactic:
Multiset.cons_zero,

Goal state after:
case cons.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih : (∀ a ∈ 0, Irreducible a) → normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ b ∈ 0, Irreducible b
⊢ normalizedFactors {a}.prod = Multiset.map normalize {a}