mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
iterate_succ_apply,

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n] (f x))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : 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
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
by_cases h : x = y

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
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

case neg
α : 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 x d = (y :: z :: zs).nextOr x d'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case zero
α : Type u_1
ts : List α
h : ts.length < 0
⊢ ts.permutations ~ ts.permutations'

Tactic:
cases h

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
this : (n + tl.length + 1) % (tl.length + 1) = n
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
simp [this]

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

Goal state before:
pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
simp [this]

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

Goal state before:
pp: case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

Tactic:
apply hyp g⁻¹ (inv_mem hg)

Goal state after:
case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inl.inr
α : 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 : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

Tactic:
exact hs.1 c (Or.inl hc)

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₂ : X
g : ↥H
this : ⋯.choose = ⋯.choose * ↑g⁻¹
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H

Tactic:
simp [this]

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

Goal state before:
pp: case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0

Tactic:
cases h

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
· exact ha.1 ((mul_mem_cancel_left hb).1 hba)

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.val < n✝ + 1

Tactic:
exact Fin.is_lt a

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
this : ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
rcases this with ⟨n₁, n₂, hlt, hle, he⟩
    refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
    rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
    rw [← zpow_natCast]
    convert! he
    lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0

Tactic:
rintro ⟨han, ⟨ha, han'⟩, rfl⟩
    simp [Nat.mul_div_eq_iff_dvd, han]
    lia

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range (n + 1), x ^ i

Tactic:
simp only [Nat.even_add_one, geom_sum_succ]

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val

Tactic:
cases n
  · simpa [ZMod.val] using! Int.natAbs_add_le _ _
  · simpa [ZMod.val_add] using! Nat.mod_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 + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
⊢ if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i

Tactic:
simp only [Nat.even_add_one, geom_sum_succ]

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ 1⁻¹ = 1

Tactic:
obtain rfl | hn := eq_or_ne n 1
  · exact Subsingleton.elim _ _
  · simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

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

Goal state before:
pp: p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ ¬IsUnit ↑p

Tactic:
by
  simp [isUnit_prime_iff_not_dvd hp]
  lia

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

Goal state before:
pp: n k : ℕ
⊢ (n + k).choose k ≤ (n + 1) ^ k

Tactic:
rw [choose_eq_asc_factorial_div_factorial]
  exact Nat.div_le_of_le_mul (ascFactorial_le_factorial_mul_pow _ _)

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
linarith

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

Goal state before:
pp: b : ℕ
l : List ℕ
this :
  List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i ↦ b * (a * b ^ i)) l (List.range l.length)
⊢ (List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i ↦ a * b ^ i) l (List.range l.length)).sum

Tactic:
simp [this]

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

Goal state before:
pp: b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ 0 < b + 2

Tactic:
linarith

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this✝ : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
this : hd < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
linarith

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b

Tactic:
tauto

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

Goal state before:
pp: case ind
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i]?.getD 0 = n.succ / (b + 2) ^ i % (b + 2)

Tactic:
rcases i with _ | i
    · rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp
    · simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

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

Goal state before:
pp: case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b

Tactic:
linarith

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
cases h

Goal state after:
case inl
a b : ℕ
h✝ : a = 1
⊢ ∀ (n : ℕ), a ^ n ∣ b

case inr
a b : ℕ
h✝ : b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
emultiplicity_eq_emultiplicity_iff

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L ≠ []

Tactic:
by
  obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
  exact cons_ne_nil d _

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
linarith

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

Goal state before:
pp: p n : ℕ
x✝¹ : 0 ≤ n
x✝ : 0 ≠ 0
⊢ n.factorization p ≤ (n.choose 0).factorization p + (factorization 0) p

Tactic:
tauto

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
linarith

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

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 1 < ↑1

Tactic:
rw [Prime.emultiplicity_one]

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n % ↑(Nat.card G)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]

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

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ (∏ i ∈ k.primeFactors, i) ^ n ∣ k ^ n

Tactic:
prod_primeFactors_dvd

Goal state after:
case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ k ^ n ∣ k ^ n
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
one_smul

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

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

Tactic:
exact le_antisymm key h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
one_smul

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

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x = 0

Tactic:
rw [orderOf_eq_zero_iff']

Goal state after:
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
have coprime : m'.Coprime n' := by
    rcases hmn with hm | hn
    · exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)
    · exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)

Goal state after:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = 0

Tactic:
· rw [Finset.sum_eq_zero]
    intro k _
    rw [if_neg]
    exact fun hkn => h ⟨k, hkn.symm⟩

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ ⊤ = ⊤ + q.trailingDegree

Tactic:
top_add

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial
R : Type u
inst✝ : Semiring R
g : R[X]
m : ℕ
a : R
⊢ derivative ((monomial m) a * g) = derivative ((monomial m) a) * g + (monomial m) a * derivative g

Tactic:
induction g using Polynomial.induction_on' with
  | add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
  | monomial n b => ?_

Goal state after:
case monomial.monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ derivative ((monomial m) a * (monomial n) b) =
    derivative ((monomial m) a) * (monomial n) b + (monomial m) a * derivative ((monomial n) b)
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
by simpa [degree_eq_natDegree hq.ne_zero] using! h0q

Goal state after:
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
x : A
a✝ : R[X]
⊢ ¬(a✝ ≠ 0 ∧ (aeval x) a✝ = 0) ↔ (aeval x) a✝ = 0 → a✝ = 0

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ s • 1 • eval₂ C q p = s • eval₂ C q p

Tactic:
one_smul

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ s • eval₂ C q p = s • eval₂ C q p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p /ₘ 1 = p

Tactic:
by
  conv_rhs => rw [← modByMonic_add_div p 1]; simp

Goal state after:
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 - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p

Tactic:
eval₂_mul,

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 q * eval₂ f x (p /ₘ q) = eval₂ f x p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)

Tactic:
have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)

Goal state after:
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this : ∀ (i : ℕ), x' i ∈ f
⊢ ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i ↦ s (x i)
Module: Mathlib.Algebra.Polynomial.Div

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

pp: case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
· rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
          ⟨by
            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div],
            (degree_add_le _ _).trans_lt
              (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
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:
simp [mul_assoc, mul_left_comm]

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
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
⊢ x ∈ s i

Tactic:
have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)

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
x : α i
hx : x ∈ t i
this : ∀ (i : ι), (t i).Nonempty
⊢ x ∈ s i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n * X)) = eval₂ C q (derivative (C r * X ^ n * X)) * derivative q

Tactic:
eval₂_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n) * eval₂ C q X) = eval₂ C q (derivative (C r * X ^ n * X)) * derivative q
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = ((f - single i 1).sum fun i c ↦ c • w i) + (single i 1).sum fun i c ↦ c • w i

pp: case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

pp: case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a

Tactic:
sum_single_index,

Goal state after:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = ((f - single i 1).sum fun i c ↦ c • w i) + 1 • w i

σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
⊢ p.prod ≤ q.prod

Tactic:
have := Classical.decEq (Associates M)
  suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
  suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
  exact mul_mono (le_refl p.prod) one_le

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
classical
  rw [← count_pos, count_roots p, rootMultiplicity_pos']

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

Goal state before:
pp: case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ ∀ x_1 ∈ normalizedFactors x + normalizedFactors y, Irreducible x_1

Tactic:
intro x hx
    rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ {↑a⁻¹ * -b} = {-(↑a⁻¹ * b)}

Tactic:
mul_neg

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ {-(↑a⁻¹ * b)} = {-(↑a⁻¹ * b)}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ n • p.roots + p.roots = n • p.roots + 1 • p.roots

Tactic:
one_smul

Goal state after:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ n • p.roots + p.roots = n • p.roots + p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ p, p ∈ factors x

Tactic:
obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
  obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x
  exact ⟨p, hp⟩

Goal state after: