mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast

Tactic:
symm

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast + b.cast = (a + b).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast

Tactic:
symm

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast * b.cast = (a * b).cast
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ {d ∈ range n.succ | d ∣ n} ↔ a✝ ∈ n.divisors

Tactic:
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]

Goal state after:
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n.succ → 1 ≤ a✝
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ n ∣ 1 ↔ n = 1

Tactic:
Nat.dvd_one

Goal state after:
n : ℕ
⊢ n = 1 ↔ n = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
symm

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 = ∑ x ∈ (n + 1 + 1).properDivisors, x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ n.properDivisors, x = 1 ↔ Prime n

Tactic:
rcases n with - | n
  · simp [Nat.not_prime_zero]
  · cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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

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

Tactic:
range_eq_Ico,

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ Ico 0 n.succ, a / b ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
by
  ext ⟨n1, n2⟩
  rw [Nat.mem_divisorsAntidiagonal]
  simp only [ne_eq, Finset.mem_filter, Finset.mem_product, Finset.mem_Ioc]
  constructor
  · intro ⟨rfl, hn2⟩
    grw [← hn]
    simp (disch := lia) only [le_mul_iff_one_le_right, le_mul_iff_one_le_left, and_true]
    lia
  · intro ⟨⟨hn1, hn2⟩, hn3⟩
    exact ⟨hn3, n_ne_zero⟩

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

Goal state before:
pp: m n : ℕ
⊢ ∀ (a : (ZMod 2)ˣ), a = 1

Tactic:
decide

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

Goal state before:
pp: case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

pp: case succ.mp.succ
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
· rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)

Goal state after:
case succ.mp.succ
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n✝ : ℕ
h : 1 < 0
⊢ ¬1 < 0

Tactic:
decide

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

Goal state before:
pp: n✝ : ℕ
h : 1 < 1
⊢ ¬1 < 1

Tactic:
decide

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

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs

Tactic:
rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ (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:
suffices
    l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
      l.zipWith (fun a i => b * (a * b ^ i)) (List.range l.length)
    by simp [this]

Goal state after:
b : ℕ
l : List ℕ
⊢ 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)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 ⊤ = 1

Tactic:
decide

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
by_contra! nh
  obtain ⟨c, hc⟩ := hf
  simp_all [dvd_add]

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ n.factorization p = 0

Tactic:
by simp [factorization_eq_zero_iff, hp]

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

Goal state before:
pp: p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r

Tactic:
← Nat.dvd_add_iff_right (Dvd.intro i rfl)

Goal state after:
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ r
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
← prod_factorization_pow_eq_self hd

Goal state after:
case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ (d.factorization.prod fun x1 x2 ↦ x1 ^ x2) ∣ n.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 0 = {[]}

Tactic:
by
  ext
  simp [fixedLengthDigits]
  grind

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ 1
⊢ False

Tactic:
Nat.dvd_one

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ multiplicity p a = 0

Tactic:
apply Nat.eq_zero_of_not_pos
  intro nh
  have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
  have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
  have := Nat.dvd_gcd da db
  rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this
  exact hp this

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

Goal state before:
pp: k m p : ℕ
hp : Prime p
⊢ m / p ^ m.factorization p = m ↔ m = 0 ∨ ¬p ∣ m

Tactic:
ordCompl_eq_self_iff_zero_or_not_dvd m hp

Goal state after:
k m p : ℕ
hp : Prime p
⊢ m = 0 ∨ ¬p ∣ m ↔ m = 0 ∨ ¬p ∣ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
n : ℕ
⊢ a ^ n ∈ ↑(powers a)

Tactic:
by simp [mem_powers_iff]

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

Goal state before:
pp: case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n

Tactic:
rw [← factorization_prime_le_iff_dvd hd hn]

Goal state after:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
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
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0

Tactic:
intro m hm

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ emultiplicity p m = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
n : ℕ
⊢ a ^ n ∈ ↑(powers a)

Tactic:
by simp [mem_powers_iff]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1

Tactic:
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
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
⊢ Prime 2

Tactic:
decide

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n

Tactic:
apply Finset.prod_subset_one_on_sdiff

Goal state after:
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}

case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1

case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ⊥ < (C ((C (p.coeff 0)).coeff 0)).degree
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 < 1

Tactic:
decide

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ ¬0 < ⊥

Tactic:
decide

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ derivative ((expand R p) f) = (expand R p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
coe_expand,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ derivative (eval₂ C (X ^ p) f) = eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
coe_expand,

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ (eval₂ C (X ^ 0) f).natDegree = f.natDegree * 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ ↑q.natDegree ≤ p.degree

Tactic:
← degree_eq_natDegree hq0

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (C p.leadingCoeff).leadingCoeff

Tactic:
leadingCoeff_C

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (p %ₘ q).degree < q.degree

Tactic:
unfold modByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree →
    (if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).2
        else p).degree <
      q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
eval_divByMonic_eq_trailingCoeff_comp

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
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (p %ₘ q).degree < q.degree

Tactic:
unfold modByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).2
      else p).degree <
    q.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p %ₘ 0 = p

Tactic:
unfold modByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p %ₘ q = p

Tactic:
unfold modByMonic divModByMonicAux

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if hq : q.Monic then
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
⊢ 0 < 1

Tactic:
decide

Goal state after:
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 (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f) = f ^ p ^ (k + 1)

Tactic:
symm

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
⊢ f ^ p ^ (k + 1) = map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a (X - C x) + rootMultiplicity a (p /ₘ (X - C x))

Tactic:
rootMultiplicity_X_sub_C,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + rootMultiplicity a (p /ₘ (X - C x))
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
⊢ Transcendental R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
Transcendental,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ ¬IsAlgebraic R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) (map (algebraMap R A) p) = 0

Tactic:
← mapAlg_eq_map,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) ((mapAlg R A) p) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Tactic:
conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ i ∈ ((⇑derivative)^[k] p).support, C (((⇑derivative)^[k] p).coeff i) * X ^ i =
    ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
Icc_eq_empty (Nat.lt_succ_iff.mpr h).not_ge,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ ∅, a ^ (i - (n + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1

Tactic:
decide

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
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
⊢ False

Tactic:
have hm : m + 1 = p.natDegree := tsub_add_cancel_of_le (by lia)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1

Tactic:
decide

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
refine ⟨I, Ifin, V, V_in, ?_⟩

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = ⋂ i, V i
Module: Mathlib.Order.Filter.Pi

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

Tactic:
rw [pi_def, biInter_eq_iInter]
  refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl
  exact preimage_mem_comap (h i i.2)

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) →
    ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ x, V ↑x ∧ U = ⋂ i, V i

Tactic:
rintro ⟨I, If, V, hV, rfl⟩

Goal state after:
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ∃ I_1,
    I_1.Finite ∧
      ∃ V_1, (∀ (i : ι), V_1 i ∈ s i) ∧ (∀ i ∉ I_1, V_1 i = univ) ∧ ⋂ i, V i = ⋂ x, V_1 ↑x ∧ ⋂ i, V i = ⋂ i, V_1 i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ ¬1 = 0

Tactic:
decide

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)

Tactic:
rw [sup_comm a, inf_comm]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)