mathlib-initiative/mathlib-tactics huggingface dataset:
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] ⋯ = (l.rotate 1)[k]

Tactic:
← getElem_pmap l.reverse.prev fun _ h => 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
⊢ (pmap l.reverse.prev l.reverse ⋯)[l.length - 1 - k] = (l.rotate 1)[k]

α : 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.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1

Tactic:
simp only [mk''_eq_coe, nodup_coe_iff] at h

Goal state after:
case h
α : Type u_1
a✝ : List α
h : a✝.Nodup
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])

Tactic:
exact
    ⟨fun b hb => by grind,
      pairwise_append.2
        ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc),
          pairwise_singleton r a, fun b hb c hc => by grind⟩⟩

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

Goal state before:
pp: case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

Tactic:
exact hs.2.2 b hb

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

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

Tactic:
rw [h₁]
    refine (prod_primeFactorsList ?_).symm
    rintro rfl
    rw [prod_eq_zero_iff] at h₁
    exact Prime.ne_zero (h₂ 0 h₁) rfl

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

Goal state before:
pp: k n : ℕ
hk : k ≠ 0
⊢ (n ^ k).primeFactors = n.primeFactors

Tactic:
cases k
  · simp at hk
  rw [primeFactors_pow_succ]

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'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ ((comap f H).subgroupOf K).index = H.relIndex (map f K)

Tactic:
subgroupOf,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ (comap K.subtype (comap f H)).index = H.relIndex (map f K)
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'
H K : Subgroup G
hf : Injective ⇑f
⊢ (comap f (map f H)).relIndex K = H.relIndex K

Tactic:
Subgroup.comap_map_eq_self_of_injective hf

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
hf : Injective ⇑f
⊢ H.relIndex K = H.relIndex K
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'
hf : Injective ⇑f
⊢ (H ⊔ ⊥).index * f.range.index = H.index * f.range.index

Tactic:
sup_bot_eq

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Injective ⇑f
⊢ H.index * f.range.index = H.index * f.range.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val < n

Tactic:
cases n
  · cases NeZero.ne 0 rfl
  exact Fin.is_lt a

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

Goal state before:
pp: n a : ℕ
⊢ (↑a).val = a % n

Tactic:
cases n
  · rw [Nat.mod_zero]
    exact Int.natAbs_natCast a
  · apply Fin.val_natCast

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

Goal state before:
pp: a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
rcases a with - | a

Goal state after:
case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0

case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
rw [ZMod.intCast_eq_intCast_iff]
  apply Int.mod_modEq

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n x y : ℕ
hn : n ≠ 0
⊢ (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
← prod_image

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1

Tactic:
· apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

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

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

Tactic:
apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (0 :: l).reverse = ofDigits b l.reverse

Tactic:
simp only [List.reverse_cons, ofDigits_append_zero]

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

Goal state before:
pp: case succ.zero.succ
n : ℕ
ih : ofDigits (0 + 1) ((0 + 1).digits n) = n
⊢ ofDigits (0 + 1) ((0 + 1).digits (n + 1)) = n + 1

Tactic:
Nat.zero_add

Goal state after:
case succ.zero.succ
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
k : ℕ
⊢ padicValNat p (p ^ k) = k

Tactic:
by
  simp [padicValNat, hp]

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

Goal state before:
pp: b m : ℕ
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits (b + 2) m]

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

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (List.take (i + 1) (hd :: tl))

Tactic:
List.take_succ_cons,

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (hd :: List.take i tl)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]

Goal state after:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑(ofDigits b' (b'.digits n)) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ emultiplicity a (-b) = emultiplicity a b

Tactic:
rw [emultiplicity_eq_emultiplicity_iff]

Goal state after:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
by
                  rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy
                  simp [hy, pow_add, mul_comm, mul_left_comm]

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ d.factorization ≤ n.factorization

Tactic:
hprod,

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization ≤ n.factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p ↔ a.factorization p ≤ b.factorization p

Tactic:
obtain _ | _ | p := p <;> simp [Nat.pow_dvd_pow_iff_le_right]

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

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

Tactic:
factorization_factorial hp ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)),

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, n / p ^ i)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

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

Goal state before:
pp: case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

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

Goal state before:
pp: case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
· simp [choose_eq_zero_of_lt hnk]

Goal state after:
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1

Tactic:
rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
    exact
      lt_of_le_of_lt
        (add_le_add
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk'))
            ((n - k) % p)))
        (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst✝ : CharP R p
x : R
⊢ orderOf x = 2 ↔ x = -1

Tactic:
simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
    and_iff_left_iff_imp]
  rintro rfl
  exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

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

Goal state before:
pp: case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

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

Goal state before:
pp: case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
· simp [choose_eq_zero_of_lt hnk]

Goal state after:
case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
u : Gˣ
⊢ IsOfFinOrder ↑u

Tactic:
Units.isOfFinOrder_val

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
u : Gˣ
⊢ IsOfFinOrder u
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
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_not_dvd, ih]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ 1 ∈ S ^ card G

Tactic:
rw [← pow_card_eq_one]

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ ?m.40 ^ card G ∈ S ^ card G

G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ G
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
⊢ (f + g).coeff n = a + b

Tactic:
by subst ‹_› ‹_›; apply coeff_add

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f✝ f g : R[X]
ihf : (expand R p) ((expand R q) f) = (expand R (p * q)) f
ihg : (expand R p) ((expand R q) g) = (expand R (p * q)) g
⊢ (expand R (p * q)) f + (expand R p) ((expand R q) g) = (expand R (p * q)) f + (expand R (p * q)) g

Tactic:
ihg

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ f + (expand R 1) g = f + g

Tactic:
ihg

Goal state after:
R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ f + g = f + g
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
rootMultiplicity_eq_natTrailingDegree,

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ ((p * q).comp (X + C x)).natTrailingDegree =
    (p.comp (X + C x)).natTrailingDegree + (q.comp (X + C x)).natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f + g) = contract p f + contract p g

Tactic:
ext; simp_rw [coeff_add, coeff_contract hp, coeff_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff (0 / p))
⊢ IsUnit f

Tactic:
p.zero_div

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsAlgebraic R A
⊢ Nontrivial R

Tactic:
obtain ⟨p, hp, -⟩ := Algebra.IsAlgebraic.isAlgebraic (R := R) (0 : A)
  exact .of_polynomial_ne hp

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 ∣ p
⊢ p %ₘ q = 0

Tactic:
nontriviality R
    obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
    by_contra hpq0
    have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
    have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
    have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
      hpq0 <|
        leadingCoeff_eq_zero.1
          (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
    have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
    rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this
    exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
⊢ s i ∈ f i

Tactic:
rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
⊢ s i ∈ f i
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
← eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg

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

Goal state before:
pp: case refine_4
α : 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
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
have hqk := congrArg Filter.ker hq.2.2
    rw [ker_sup, ker_principal, le_cofinite_iff_ker.mp hq.1, union_empty] at hqk
    refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)
    · rw [hq.2.2]
      exact le_sup_right
    · rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]
      exact hq.2.1
    · grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]
      exact Coheyting.boundary_le

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)

Tactic:
by
  rw [derivative_pow, derivative_X_sub_C, mul_one]

Goal state after:
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
⊢ ∑ T ∈ powersetCard (#S - k) S, derivative (∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - k) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
congr! with T hT

Goal state after:
case 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
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ derivative (∏ a ∈ T, (X - C a)) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr
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}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
· rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩
      · rw [hc]; rw [hc, mul_assoc] at hprod
        refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
        · right; exact ha₂
        rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
        exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
      rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
      refine hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
      rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
      exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
cases subsingleton_or_nontrivial α
  · obtain rfl : s = 0 := by
      apply Multiset.eq_zero_of_forall_notMem
      intro _
      convert! hs
    simp
  induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
simp [hy]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a

Tactic:
rcases a with - | a

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0

case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Goal state after: