mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
⊢ v ∈ ((aeval f) (p * q)).ker → v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker

Tactic:
hv

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ ((aeval f) (p * q)).ker
⊢ v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)

Tactic:
exact Int.dvd_sub h₂.dvd h₁.dvd

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hc : c ≠ 0
⊢ m * c ∣ (b - a) * c → m ∣ b - a

Tactic:
exact Int.dvd_of_mul_dvd_mul_right hc

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
⊢ InjOn Int.cast (Ico 0 ↑p)

Tactic:
rintro a ⟨ha₀, ha⟩ b ⟨hb₀, hb⟩ hab

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < ↑p
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
hab : ↑a = ↑b
⊢ a = b
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: m n : ℕ
⊢ ¬m.Coprime n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
by
  apply Iff.intro
  · intro h
    exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
  · intro h
    obtain ⟨p, hp⟩ := h
    apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2

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

Goal state before:
pp: α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup

Tactic:
← Finset.coe_toList l

Goal state after:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ (↑l.toList).lists.Nodup
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Injective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

Tactic:
intro a b
    obtain ⟨⟨x, hx⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ a
    obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b
    simp [Ideal.Quotient.eq, Submodule.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ']

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (x :: l)).length + 1

Tactic:
simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ↑↑φ a = x
⊢ x ∈ φ.range

Tactic:
exact ⟨a, ha⟩

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

Goal state after:
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
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (Disjoint on permutations'Aux x) as bs
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) =
    Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
← MulEquiv.toMonoidHom_eq_coe

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a) =
    Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ = s.prev hs x hx

Tactic:
simp [← prev_reverse_eq_next]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.next hs x hx = s.prev ⋯ x ⋯

Tactic:
simp [← prev_reverse_eq_next]

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
by
  rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]

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

Goal state before:
pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
· rw [primeFactorsList] at h
      injection h

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
by
  rcases a.eq_zero_or_pos with (rfl | ha)
  · simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  · simp [(coprime_zero_right _).mp hab]
  exact perm_primeFactorsList_mul ha.ne' hb.ne'

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).relIndex H = K.relIndex H

Tactic:
inf_relIndex_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K.relIndex H = K.relIndex H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * (K ⊓ L).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
inf_relIndex_right

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
dsimp [ZMod, ZMod.cast]

Goal state after:
case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

Tactic:
dsimp [ZMod, ZMod.cast]

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
dsimp [ZMod, ZMod.cast]

Goal state after:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
nzm : NeZero m
h : m ≤ n
⊢ Injective cast

Tactic:
by
  cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f

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

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

Tactic:
by
  have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
  induction n with
  | zero => simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]
  | succ n ih =>
    simp only [Nat.even_add_one, geom_sum_succ]
    split_ifs at ih ⊢ with h
    · rw [le_add_iff_nonneg_left]
      exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
    · grw [← hx]
      gcongr
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a b : ℕ
c : a < b
d : ℕ × ℕ
h :
  (have y := n / a;
    if a * y = n then some (a, y) else none) =
    some d
ha : ℕ × ℕ
h' :
  (have y := n / b;
    if b * y = n then some (b, y) else none) =
    some ha
⊢ d.1 < ha.1

Tactic:
rw [Option.ite_none_right_eq_some, Option.some.injEq] at h h'

Goal state after:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ (a, n / a) = d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ (b, n / b) = ha
⊢ d.1 < ha.1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ↑1 = 0 ↔ n = 1

Tactic:
natCast_eq_zero_iff,

Goal state after:
n : ℕ
⊢ n ∣ 1 ↔ n = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
rw [neg_val']

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

Tactic:
by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]

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

Goal state before:
pp: case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0

Tactic:
intro h
          exact h (AddSubgroup.mem_zmultiples _)

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

Goal state before:
pp: case cons.w₁
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
l : ℕ
⊢ l ∈ L → l < b

Tactic:
m

Goal state after:
case cons.w₁
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
l : ℕ
m : l ∈ L
⊢ l < b
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

pp: case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
· exact Prod.ext hk.symm h.symm

Goal state after:
case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case nil
b : ℕ
⊢ ofDigits b [] % b = [].head! % b

Tactic:
simp [Nat.ofDigits]

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

Goal state before:
pp: case cons
b head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofDigits b tail✝ % b = tail✝.head! % b
⊢ ofDigits b (head✝ :: tail✝) % b = (head✝ :: tail✝).head! % b

Tactic:
simp [Nat.ofDigits]

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

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d + b' * ofDigits b' L) % ↑k

Tactic:
rw [Int.add_emod, Int.mul_emod]

Goal state after:
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

Tactic:
induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h),

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ 1) = orderOf y
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rcases em' p.Prime with (pp | pp); · simp [pp]
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rw [pow_dvd_pow_iff_le_right pp.one_lt]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab p

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
h.add_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * ↑((p ^ n).choose m) =
    ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ multiplicity p (p ^ n)! = ∑ i ∈ range n, p ^ i

Tactic:
← ENat.natCast_inj,

Goal state after:
n p : ℕ
hp : Prime p
⊢ ↑(multiplicity p (p ^ n)!) = ↑(∑ i ∈ range n, p ^ i)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ (∏ p ∈ n.primeFactors, p) ^ n

Tactic:
nth_rw 1 [← Finset.prod_pow, prod_primeFactors_pow_factorization hn]
  refine prod_dvd_prod_of_dvd _ _ fun i hi ↦ pow_dvd_pow i ?_
  grw [n.factorization_def <| prime_of_mem_primeFactors hi, padicValNat_le_self]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
rw [of'_mul_modOf]

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (f.coeff 0)

Tactic:
apply hc <;> simp

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]
s : S
hp : (aeval s) p = 0
hq : (aeval s) q = 0
w✝¹ w✝ : R[X]
h : w✝¹ * p + w✝ * q = 1
⊢ False

Tactic:
apply_fun aeval s at h

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]
s : S
hp : (aeval s) p = 0
hq : (aeval s) q = 0
w✝¹ w✝ : R[X]
h : (aeval s) (w✝¹ * p + w✝ * q) = (aeval s) 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = C a ^ p * (X ^ n) ^ p

Tactic:
← C.map_pow,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
nontriviality S
  have : Nontrivial R := f.domain_nontrivial
  have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
    div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
        calc
          _ ≤ degree (p %ₘ q) := degree_map_le
          _ < degree q := degree_modByMonic_lt _ hq
          _ = _ :=
            Eq.symm <|
              degree_map_eq_of_leadingCoeff_ne_zero _
                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
  exact ⟨this.1.symm, this.2.symm⟩

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

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
coeff_divByMonic_X_sub_C_rec,

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⊤ = ⨅ i, f (x i)

Tactic:
use fun _ => i₀

Goal state after:
case h
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ i, f ((fun x ↦ i₀) i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ derivative (p ^ (n.succ + 1)) = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
by
    rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
      add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]; simp [add_mul]

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i

Tactic:
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩

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

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

Tactic:
by
  rw [derivative_pow, 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]
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] (X ^ m)) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
iterate_derivative_X_pow_eq_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)) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢∂ a = ⊤

Tactic:
rw [boundary, hnot_inf_distrib, sup_hnot_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : i ∉ range f
⊢ mapDomain f v i = 0

Tactic:
rw [← Set.preimage_singleton_eq_empty] at h'
  simp [mapDomain, Set.Finite.toFinset, h']

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ Multiset.prod 0 ~ᵤ a → (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}

Tactic:
intro h; exact (ha.not_isUnit (associated_one_iff_isUnit.1 (Associated.symm h))).elim

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

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

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

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : m.Nodup
⊢ { val := m, nodup := hm }.prod f ≠ 0 →
    ({ val := m, nodup := hm }.prod f).roots = { val := m, nodup := hm }.val.bind fun i ↦ (f i).roots

Tactic:
simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n - C 0).roots = replicate n 0

Tactic:
C.map_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n - 0).roots = replicate n 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
n : ℕ
s : Set α
⊢ n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
classical
  induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ % q = p₁ % q * (p₂ % q) % q

Tactic:
simp_rw [Polynomial.mod_def]

Goal state after:
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ %ₘ (q * C q.leadingCoeff⁻¹) =
    p₁ %ₘ (q * C q.leadingCoeff⁻¹) * (p₂ %ₘ (q * C q.leadingCoeff⁻¹)) %ₘ (q * C q.leadingCoeff⁻¹)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
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
hp0 : ¬p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

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]
hq : q ≠ 0
⊢ p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
constructor
  · rintro ⟨r, rfl⟩
    rw [(associated_content_mul ..).dvd_iff_dvd_right,
      p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]
    exact ⟨dvd_mul_right .., dvd_mul_of_dvd_left p.primPart_dvd _⟩
  · rintro ⟨h₁, h₂⟩
    rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
    gcongr

Goal state after: