mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]

Tactic:
simp_rw [← sub_eq_add_neg, sub_self]; rfl

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case e'_1
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.24 * (m / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case e'_2
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case e'_3
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)

Tactic:
rwa [Int.mul_ediv_cancel']

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ a + b [ZMOD n] ↔ n ∣ b

Tactic:
modEq_comm,

Goal state after:
n a b : ℤ
⊢ a + b ≡ a [ZMOD n] ↔ n ∣ b
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ b ≡ a + b [ZMOD n] ↔ n ∣ a

Tactic:
modEq_comm,

Goal state after:
n a b : ℤ
⊢ a + b ≡ b [ZMOD n] ↔ n ∣ a
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R

Tactic:
simpa using h p hp

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n

Tactic:
intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (↑(centralizer R s) ∪ ↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer

Tactic:
Set.union_self,

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer
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.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).mul_const _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (pmap l.next l ⋯)[k]

Tactic:
pmap_next_eq_rotate_one _ h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (l.rotate 1)[k]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y

Tactic:
| _ l
   => 

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]
    refine ⟨hd, hd', ?_, by simp⟩
    simp only [not_or, mem_cons, nodup_cons] at hl
    exact hl.left.left

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

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

Tactic:
| _ l
   => 

Goal state after:
case h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
ext; simp [stabilizerEquivStabilizer_apply, H]

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

Goal state before:
pp: case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)

Tactic:
| _ l
   => 

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.next y hm = l₂.next y hm'

Tactic:
simpa using isRotated_next_eq h h₁ _

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

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
by
  cases n <;> simp [mem_primeFactorsList, *]

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

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k

Tactic:
rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card G' ∣ Nat.card G

Tactic:
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
  exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 0 ↔ Infinite (G ⧸ H)

Tactic:
by
  simp [index_eq_card, Nat.card_eq_zero]

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

Goal state before:
pp: m n : ℕ
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
suffices (m % n).gcd n = m.gcd n by grind
  exact Nat.ModEq.gcd_eq (by simp [Nat.ModEq])

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i

Tactic:
by
      rw [pow_zero, Nat.div_one]

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

Goal state before:
pp: n : ℕ
⊢ Nontrivial (ZMod n) ↔ n ≠ 1

Tactic:
by
  rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ -x = x

Tactic:
simp [add_self, eq_comm, ← sub_eq_zero]

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
· have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
    rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
    refine Nat.succ_le_of_lt (log_pos hb ?_)
    contrapose! h
    exact div_eq_of_lt h

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

Goal state before:
pp: case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
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

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
unfold emultiplicity at hk

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l i : ℕ
x✝² : i ∈ ↑(Finset.range b)
j : ℕ
x✝¹ : j ∈ ↑(Finset.range b)
x✝ : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j
⊢ i = j

Tactic:
rw [Finset.mem_inter] at hL

Goal state after:
b : ℕ
hb : 1 < b
l i : ℕ
x✝² : i ∈ ↑(Finset.range b)
j : ℕ
x✝¹ : j ∈ ↑(Finset.range b)
x✝ : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j
⊢ i = j
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / (orderOf x / n) = n

pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
Nat.div_div_self hn hx

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ n = n

G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = ↑p * (x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p))

Tactic:
obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = ↑p * (x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))

Tactic:
obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

pp: case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
· simp [h, succ_div_of_dvd, ih]

Goal state after:
case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).natDegree = f.natDegree * p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ ↑0 < ↑p.natDegree

Tactic:
rw [← degree_eq_natDegree hp0]; exact hp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
⊢ False

Tactic:
have := congr_arg natDegree hr

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
· simp_rw [subset_iff, mem_image, mem_antidiagonal]; rintro _ ⟨x, rfl, rfl⟩; simp_rw [add_mul]

Goal state after:
case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
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 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 * p, (x, y).2 * p) = (p * x, p * y)

Tactic:
by simp_rw [mul_comm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
⊢ (⇑derivative)^[x] p = 0

Tactic:
induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | _ _ ih
   =>  _ 

Goal state after:
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0
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
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0
        rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
          degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
        exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

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

Goal state before:
pp: case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree

Tactic:
Nat.sub_add_cancel

Goal state after:
case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ q.natDegree ≤ q.natDegree

case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ p.natDegree ≤ q.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
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
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1) - 1 + 1) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i

Tactic:
Nat.sub_add_cancel

Goal state after:
case inr.refine_1.e_a.refine_2
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
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i

case inr.refine_1.e_a.refine_2
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
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 ≤ i - (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p

Tactic:
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i ↦ s i (ind i))

Tactic:
rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩

Goal state after:
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i ↦ s i (ind i))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (p.comp (X + C t)).trailingCoeff

Tactic:
← congr_arg (comp · <| X + C t) mul_eq,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (((X - C t) ^ m * g).comp (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ i ∈ I, s i ⊆ t
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
rw [biInter_eq_iInter] at hst

Goal state after:
case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ x, s ↑x ⊆ t
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)
Module: Mathlib.Order.Filter.Finite

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

Tactic:
have := hs.to_subtype
  rw [biUnion_eq_iUnion, biUnion_eq_iUnion]
  exact .iUnion fun i ↦ hle i.1 i.2

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

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

Tactic:
convert! (derivative p).iterate_derivative_mul_X_pow n 1; · simp
  rcases n with rfl | n <;> simp [sum_range_succ]

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

Goal state before:
pp: M₀ : Type u_3
M : Type u_4
inst✝ : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
exact mt (Prime.dvd_finsetProd_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

Goal state after: