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

Goal state before:
pp: case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1

Tactic:
simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff,
    Fintype.card_le_one_iff_subsingleton, Nat.add_one_le_iff, Fintype.card_pos_iff,
    Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, nonempty_orbit, implies_true]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]

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

Goal state before:
pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Tactic:
· rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = (p ^ n).primeFactorsList

Tactic:
← List.replicate_perm

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a :: replicate n a <+~ [a] ++ (a ^ n * c).primeFactorsList

Tactic:
singleton_append,

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a :: replicate n a <+~ a :: (a ^ n * c).primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : K.relIndex L ≠ 0
hH : H.relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K).relIndex L ≠ 0

Tactic:
← inf_relIndex_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ZMod 0
⊢ IsUnit n ↔ Int.natAbs n = 1

Tactic:
rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
⊢ H.index = 1 ∨ H.index = 2

Tactic:
have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

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
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
← zpow_natCast

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ i ∈ s, f i).FiniteIndex

Tactic:
rw [iInf_subtype']
  exact finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y

Tactic:
← f'.coe_toHomUnits y⁻¹,

Goal state after:
case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * ↑(f'.toHomUnits y⁻¹) = f' x ↔ f' g = f' x * f' y
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ ((algebraMap (ZMod n) R) x * y) • z = x • y • z

Tactic:
mul_smul

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
by
  rcases eq_or_ne m 0 with (rfl | hm); · simp [divisors]
  simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]
  exact le_of_dvd hm.bot_lt

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

Goal state before:
pp: n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
  rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
rw [hx, neg_one_geom_sum]

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 ≤ ∑ i ∈ range n, x ^ i ↔ ¬(Even n ∧ x + 1 < 0)

Tactic:
le_iff_lt_or_eq,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i ∨ 0 = ∑ i ∈ range n, x ^ i ↔ ¬(Even n ∧ x + 1 < 0)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1

Tactic:
le_iff_lt_or_eq,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by_cases hn : n = 0

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

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
· right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range' 0 L.length)).sum

Tactic:
← List.range_eq_range'

Goal state after:
b : ℕ
L : List ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b n : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | n

Goal state after:
case pos.zero
b : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits 0).head! = 0 % b

case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % 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
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]

Goal state after:
α : 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
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p
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 / n ≠ 0

Tactic:
← Nat.div_mul_cancel hn

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
rcases lt_or_ge n k with hnk | hkn

Goal state after:
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

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.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) ≤ ↑(n / (p - 1))

Tactic:
apply WithTop.coe_mono

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ ↑(#({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
        #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k})) ≤
    ↑n

Tactic:
apply WithTop.coe_mono

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) +
      #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ∣ k}) ≤
    n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n.factorization m = #({i ∈ Ico 1 b | m ^ i ∣ n})

Tactic:
factorization_eq_card_pow_dvd n hm,

Goal state after:
b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ #({i ∈ Ico 1 n | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)

case neg
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
use Fintype.card (G ⧸ zpowers x)
  rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]

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

Goal state before:
pp: n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 p2

Tactic:
refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_

Goal state after:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ (↑p1).Coprime ↑p2
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
hS : S.Nonempty
⊢ 1 ∈ S ^ card G

Tactic:
by
    obtain ⟨a, ha⟩ := hS
    rw [← pow_card_eq_one]
    exact Set.pow_mem_pow ha

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
wf : p.divX.degree < p.degree
⊢ M p

Tactic:
rw [← divX_mul_X_add p] at *

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
⊢ M (p.divX * X + C (p.coeff 0))
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m

Tactic:
subst h h_pow_bas

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
m n : ℕ
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
rw [mul_smul_comm, ← smul_add, modByMonic_add_div]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

Tactic:
let : Invertible a := ha.invertible
  apply le_antisymm (rootMultiplicity_comp_C_mul_X_add_C_le p a b c ha)
  have := rootMultiplicity_comp_C_mul_X_add_C_le
    (p.comp (C a * X + C b)) ⅟a (- ⅟a * b) (a * c + b) (isUnit_of_invertible ⅟a)
  simpa [comp_assoc, mul_add, ← mul_assoc, ← map_mul] using this

Goal state after:
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:
simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]

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

Goal state before:
pp: S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

Tactic:
by_contra! ⟨hp, hq⟩

Goal state after:
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hp : (aeval s) p = 0
hq : (aeval s) q = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) ((expand R p) (map (iterateFrobenius R p k) ((expand R (p ^ k)) f))) =
    map ((iterateFrobenius R p 1).comp (iterateFrobenius R p k)) ((expand R (p * p ^ k)) f)

Tactic:
← map_map,

Goal state after:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) ((expand R p) (map (iterateFrobenius R p k) ((expand R (p ^ k)) f))) =
    map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k)) f))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [hfg, natDegree_zero]
    rw [divByMonic_eq_zero_iff hg] at hfg
    rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]

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 • p).comp q = s • p.comp q

Tactic:
by
  rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s a : Set (Set α)
fina : a.Finite
suba : a ⊆ s
b : Set (Set α)
finb : b.Finite
subb : b ⊆ s
⊢ ∃ z ∈ sInter '' {t | t.Finite ∧ t ⊆ s}, z ⊆ ⋂₀ a ∩ ⋂₀ b

Tactic:
exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
        (sInter_union _ _).subset⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
⊢ p.natDegree = 0

Tactic:
natDegree_eq_zero_iff_degree_le_zero

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
⊢ p.degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
⊢ derivative ((X + C c) ^ 2) = C 2 * (X + C c)

Tactic:
by
  rw [derivative_sq, derivative_X_add_C, mul_one]

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

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

Tactic:
mul_smul

Goal state after:
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
⊢ ∑ x ∈ range n.succ, n.choose x • ((⇑derivative)^[n - x] p * ↑(m.descFactorial x) • X ^ (m - x)) =
    ∑ x ∈ range n.succ, n.choose x • m.descFactorial x • ((⇑derivative)^[n - x] p * X ^ (m - x))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ⋂ x, ⋂ (_ : p ↑x), s ↑x ⊆ ⋂ i, ⋂ (i_1 : p ↑i), t i i_1

Tactic:
gcongr with i hpi

Goal state after:
case h
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
i : ↑I
hpi : p ↑i
⊢ s ↑i ⊆ t i hpi
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Tactic:
exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]

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

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

Tactic:
rw [prod_comm, mem_map, mem_prod_iff_left]; rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set (α × β)
⊢ sᶜ ∈ cofinite.coprod cofinite ↔ sᶜ ∈ cofinite

Tactic:
by
    simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

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

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
refine ⟨a₀, ha₀s, fun a has => (lt_or_ge (f a) x).elim ?_ (le_trans ha₀.le)⟩

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
a₀ : α
others_bigger : ∀ b ∈ {y | f y < x} ∩ s, f a₀ ≤ f b
ha₀ : f a₀ < x
ha₀s : a₀ ∈ s
a : α
has : a ∈ s
⊢ f a < x → f a₀ ≤ f a