mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 ↦ x * x_1) w 1
⊢ x ^ ↑w = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
zpowersEquivZPowers,

Goal state after:
G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ((finEquivZPowers ⋯).symm.trans ((finCongr h).trans (finEquivZPowers ⋯))) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : d = df + dg
⊢ (f * g).coeff d = a * b

Tactic:
subst h_mul_left h_mul_right h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
h_mul_left : f.natDegree ≤ df
h_mul_right : g.natDegree ≤ dg
ddf : df + dg ≤ df + dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ f.coeff d = 0

Tactic:
by
    simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_gt hd, IsEmpty.forall_iff]

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

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

Tactic:
comp_X_add_C_eq_zero_iff

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ (if p = 0 then 0 else multiplicity (X - C t) p) = if p = 0 then 0 else multiplicity (X - C 0) (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (((expand R p) q).coeff n✝) = ((expand S p) (map f q)).coeff n✝

Tactic:
coeff_expand (Nat.pos_of_ne_zero hp),

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = ((expand S p) (map f q)).coeff n✝
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
intro _ H
      rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]

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

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

Tactic:
have _wf := div_wf_lemma h hq

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
⊢ p %ₘ q = p - q * (p /ₘ q)
Module: Mathlib.Algebra.Polynomial.RingDivision

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

Tactic:
rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
← map_natCast C n

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (C ↑n) = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = 1

Tactic:
rw [← C_1]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = C 1
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
⊢ p /ₘ q = 0

Tactic:
by
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
| (aeval x) p = 0

Tactic:
← h.eq_iff,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
| S.val ((aeval x) p) = S.val 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ eval a p = 0

Tactic:
rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
⊢ (X - C a) * (p /ₘ (X - C a)) = p

Tactic:
conv_rhs => rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : α → Set β
hpf : ∀ a ∈ s, p a ∈ f a
⊢ ⋂ x, p ↑x ∈ ⨅ x, f ↑x

Tactic:
exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

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

Goal state before:
pp: α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
this : ∀ (i : ι), (f₂ i).NeBot
⊢ f₁ = f₂

Tactic:
exact hle.antisymm (pi_le_pi.1 h.ge)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Tactic:
Filter.pure_prod

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
    ∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)

Tactic:
apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)

Goal state after:
case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match
        match a, ha with
        | (T, i), x => (T.erase i, i),
        ⋯ with
      | (T, i), x => (insert i T, i)) =
      a

case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match
        match a, ha with
        | (T, i), x => (insert i T, i),
        ⋯ with
      | (T, i), x => (T.erase i, i)) =
      a

case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
      match
        match a, ha with
        | (T, i), x => (T.erase i, i) with
      | (T, i) => ∏ a ∈ T, (X - C a)

case hi
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a, ha with
      | (T, i), x => (T.erase i, i)) ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match x with
        | (T, i) => i ∉ T}

case hj
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match a, ha with
      | (T, i), x => (insert i T, i)) ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match x with
        | (T, i) => i ∈ T}
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
⊢ derivative P = 0

Tactic:
by_cases hP : P = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : P = 0
⊢ derivative P = 0

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f

Tactic:
· simp only [notMem_support_iff] at h
    simp only [h, zero_le]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map normalize s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ b ∈ s, Irreducible b
b : α
hb : b ∈ s
this : Nontrivial α
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map normalize (a ::ₘ s)

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons,
      normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
      normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ nthRoots 2 1 = {-1, 1}

Tactic:
have h₁ : (X ^ 2 - C 1 : R[X]) = (X + C 1) * (X - C 1) := by simp [← sq_sub_sq]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
⊢ nthRoots 2 1 = {-1, 1}
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
by_cases h0 : r = 0; · simp [h0]
  refine .trans (.of_eq ?_) (Finset.gcd_mul_left' _ _ _)
  rw [content]; refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ↑((C a).aroots S).toFinset = ∅

Tactic:
aroots_C,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ↑(toFinset 0) = ∅
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (-p).rootSet S = p.rootSet S

Tactic:
by
  rw [rootSet, aroots_neg, rootSet]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ C r * C ↑(normUnit r) * C ↑(normUnit r)⁻¹ = C r

Tactic:
rw [mul_assoc, ← map_mul, Units.mul_inv, C_1, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (aeval s) p = 0
⊢ (aeval s) p.primPart = 0

Tactic:
by
  nontriviality S
  rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  have : IsDomain R := { Module.nontrivial R S with }
  rwa [(FaithfulSMul.algebraMap_injective R S).ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = (Multiset.map Subtype.val a).prod * (Multiset.map Subtype.val b).prod

Tactic:
Multiset.map_add,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val a + Multiset.map Subtype.val b).prod =
    (Multiset.map Subtype.val a).prod * (Multiset.map Subtype.val b).prod
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ g ≠ 0

Tactic:
rintro rfl; simp at hg

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

Goal state before:
pp: case neg.inl
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
hlt : (p * q).degree < ↑n
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
apply ih _ _ hlt

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C (p * q).content * (p * q).primPart

Tactic:
rw [← (p * q).eq_C_content_mul_primPart, p.eq_C_content_mul_primPart,
      q.eq_C_content_mul_primPart]

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C p.content * p.primPart * (C q.content * q.primPart)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ IsCoprime (X - C a) (f /ₘ (X - C a))

Tactic:
refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ ¬X - C a ∣ f /ₘ (X - C a)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ (C (lcm p.content q.content)).primPart * r ∣ s.primPart

Tactic:
(isUnit_primPart_C (lcm p.content q.content)).mul_left_dvd,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ r ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case e'_4
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
hα : Nontrivial α
⊢ Nat.find ⋯ = p.count (p ^ Nat.find ⋯).factors

Tactic:
count_pow hp.ne_zero hp,

Goal state after:
case e'_4
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
hα : Nontrivial α
⊢ Nat.find ⋯ = Nat.find ⋯ * p.count p.factors
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
h : p.leadingCoeff * f.leadingCoeff ^ p.natDegree = 0
⊢ p = 0

Tactic:
mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
h : p.leadingCoeff = 0
⊢ p = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
A : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul R A
⊢ FaithfulSMul S A

Tactic:
rw [faithfulSMul_iff_algebraMap_injective] at *
  exact injective_tower_top S ‹_›

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]) (a : K),
    p.coeff 0 = 0 → a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

Tactic:
intro p a hp ha _ih _ne_zero aeval_eq
    refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
    rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]

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

Goal state before:
pp: case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A

Tactic:
exact A.zero_mem

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
s : Set M
inst✝ : Small.{u, u_2} ↑s
this : span R s = ⨆ i, R ∙ ↑i
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
by
    rw [this]
    apply small_iSup

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy)).sum

Tactic:
Multiset.map_add,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx + Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
⊢ x = 0

Tactic:
by
  have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ Nat.one_pos)
  rw [← pow_nilpotencyClass this, hx, pow_one]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → One (G i)
inst✝² : One C
inst✝¹ : ∀ (i : ι), OneHomClass (H i) (G i) C
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
i : ι
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h 1 = 1

Tactic:
rw [one_def, lift_def, map_one (g i)]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : Nonempty ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ 0 * ⟦⟨i, x✝⟩⟧ = 0

Tactic:
by simp_rw [zero_def i, mul_def, zero_mul]

Goal state after: