mathlib-initiative/mathlib-tactics huggingface dataset:
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 < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1

Tactic:
clear hn

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1
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
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (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:
clear hn

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 : ℕ),
    2 ≤ n →
      (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
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x.swap.2 * x.swap.1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
Prod.swap

Goal state after:
n : ℕ
x : ℕ × ℕ
⊢ (x.2, x.1).2 * (x.2, x.1).1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
rw [← sum_sdiff hsub]
    intro h
    apply Subset.antisymm hsub
    rw [← sdiff_eq_empty_iff_subset]
    contrapose! h
    apply ne_of_lt
    rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
    gcongr
    have hlt :=
      sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
    simp only [sum_const_zero] at hlt
    apply hlt

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

Goal state before:
pp: a : ℤ
⊢ ↑|a| = ↑a

Tactic:
cases le_total a 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
n : ℕ
a : ZMod n
⊢ a + a = 0 ↔ a = 0 ∨ 2 * a.val = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
rw [digitsAux]

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m * a).val ≤ a.val ^ m * a.val

Tactic:
apply le_trans (ZMod.val_mul_le _ _)

Goal state after:
case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m).val * a.val ≤ a.val ^ m * a.val
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < n + 1

Tactic:
apply Nat.div_lt_self <;> lia

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

Goal state before:
pp: case ind.succ.tail
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d < b + 2

Tactic:
apply IH ((n + 1) / (b + 2))
    · apply Nat.div_lt_self <;> lia
    · assumption

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

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
← ofDigits_one <| digits p.succ n.succ

Goal state after:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ n < b * b ^ (e + 1)

Tactic:
rwa [← pow_add_one']

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

Goal state before:
pp: case refine_2.inl
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b

Tactic:
exact hd

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, L ∈ consFixedLengthDigits hb l a

Tactic:
consFixedLengthDigits,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, L ∈ Finset.image (fun L ↦ a :: L) (fixedLengthDigits hb l)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow

Tactic:
apply n.dvd_mul_right

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})

Tactic:
apply factorization_eq_card_pow_dvd_of_lt hp (zero_lt_succ n)
          (lt_pow_of_log_lt hp.one_lt hb)

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
⊢ n.factorization p < n

Tactic:
by
  by_cases pp : p.Prime
  · exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt
  · simpa only [factorization_eq_zero_of_not_prime n pp] using! hn.bot_lt

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
by
  have h0 : 2 ≤ p := hp.two_le
  have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
  have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
  have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
  have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 := by
    apply factorization_eq_zero_of_not_dvd
    exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right
  rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]

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

Goal state before:
pp: case mp
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
by_cases n_zero : n = 0

Goal state after:
case pos
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n

case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2

Tactic:
by
  split_ifs with h
  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
  apply orderOf_eq_prime
  · simp
  simpa [neg_one_eq_one_iff] using h

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]

Goal state after:
R : Type u_6
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst✝ : CharP R p
x : R
⊢ x = -1 → ¬x = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)

Tactic:
rintro h1 -

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x y, 1 - k * x = ↑(orderOf g) * y

Tactic:
← dvd_def,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x, ↑(orderOf g) ∣ 1 - k * x
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
coprime : m'.Coprime n'
| a ^ m

Tactic:
show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm

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'
| a ^ (m' * g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX + C (f.coeff 0)

Tactic:
X_mul_divX_add

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree 0 = natDegree 0 * p

Tactic:
natDegree_zero,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ 0 = 0 * p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - C 0) (p.comp (X + C t))

Tactic:
rw [C_0, sub_zero]

Goal state after:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity X (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0

Tactic:
exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))

Goal state after:
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)
⊢ ¬p ≠ 0 → (p %ₘ q).degree < q.degree

Tactic:
intro hp
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
          exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero))

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ natDegree 0 < q.natDegree

Tactic:
natDegree_zero,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ 0 < q.natDegree
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ (algebraMap A B) ((aeval x) p) = 0 ↔ (aeval x) p = 0

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ (aeval x) p • 1 = 0 ↔ (aeval x) 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
⊢ 0 ∈ Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)

Tactic:
rw [Multiset.map_map, Multiset.mem_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
⊢ ∃ a ∈ s, (⇑(aeval x) ∘ fun x ↦ X - C x) a = 0
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 : R[X]
x : R
⊢ eval x (s • p) = s • eval x p

Tactic:
rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]

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

Tactic:
comp,

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]
⊢ eval₂ C q ((s • 1) • p) = s • p.comp q
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]
⊢ eval₂ C q ((s • 1) • p) = s • p.comp q

Tactic:
comp,

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]
⊢ eval₂ C q ((s • 1) • p) = s • eval₂ C q p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ p %ₘ p = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hp]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ degree 0 < q.degree

Tactic:
rw [degree_zero]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) i = (Finsupp.single 0 (C r)) i

Tactic:
match i with
  | 0 => simp
  | i + 1 => simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - 1) ∣ derivative p

Tactic:
obtain ⟨r, rfl⟩ := dvd

Goal state after:
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n * r)
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, (s i)ᶜ ∈ f i) → (univ.pi s)ᶜ ∈ pi f

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
i : ι
hi : (s i)ᶜ ∈ f i
⊢ (univ.pi s)ᶜ ∈ pi f
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' x

Tactic:
intro s

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
⊢ (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s) →
    ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ (fun k i ↦ m i (k i)) ⁻¹' s
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

Tactic:
by
  refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
  rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
  exact fun x _ => h x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ), (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
intro s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Tactic:
intro s

Goal state after:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_2
α : 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
hqk : f.ker = q.1
⊢ Disjoint (𝓟 q.1) q.2

Tactic:
exact hq.2.1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
⊢ WfDvdMonoid α → WellFoundedLT (Associates α)

Tactic:
apply WfDvdMonoid.wellFoundedLT_associates

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 ↔ f = 0

Tactic:
by
  constructor
  · intro h
    ext s
    simp only [Finsupp.coe_zero, Pi.zero_apply]
    by_contra hs
    apply NonTorsionWeight.ne_zero ℕ w s
    rw [← nonpos_iff_eq_zero, ← h]
    exact le_weight_of_ne_zero' w hs
  · intro h
    rw [h, map_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
intro s

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s : Multiset α
⊢ ∀ (s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 0 r = 0

Tactic:
by
  simp only [pow_zero, nthRoots, ← C_1, ← C_sub, roots_C]

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s : Set α
⊢ ∀ (s : Set (α →₀ ℕ)),
    ((fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' (n • s)

Tactic:
intro s

Goal state after:
α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s✝ : Set α
s : Set (α →₀ ℕ)
⊢ ((fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' (n • s)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).content = p.content

Tactic:
rw [content, content, Finset.gcd_def, Finset.gcd_def]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
    rw [aroots_def, Polynomial.map_mul, roots_mul this]
  rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff
    (FaithfulSMul.algebraMap_injective T S)]

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

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ 0 < (hu.unit⁻¹ • q).degree

Tactic:
rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

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

Goal state before:
pp: case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

Tactic:
rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.eraseLead.degree < q.primPart.degree

Tactic:
apply degree_erase_lt q.primPart_ne_zero

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

Goal state before:
pp: R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x : R[X]
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)

Tactic:
simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hroots : p.roots.card = p.natDegree
⊢ Multiset.map (⇑f) p.roots = (map f p).roots

Tactic:
by
  apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
  simpa only [Multiset.card_map, hroots] using card_roots_map_le_natDegree p

Goal state after: