mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ (p ::ₘ s).prod * ↑u = p * ↑u * s.prod

Tactic:
mul_comm,

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ↑u * (p ::ₘ s).prod = p * ↑u * s.prod
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
s : Set ℕ
n : ℕ
hn : n ≠ 0
⊢ ⇑degree ⁻¹' (n • s) = n • ⇑degree ⁻¹' s

Tactic:
by
  obtain (_ | n) := n; · contradiction
  induction n <;> simp_all [succ_nsmul, degree_preimage_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X - C b).roots = {↑a⁻¹ * b}

Tactic:
rw [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
    Units.inv_mul, C_1, one_mul]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s : Set α
⊢ (f '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
by
  classical
  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
  intro s
  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = p.support.gcd p.coeff

Tactic:
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.RingTheory.Polynomial.Content

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
mul_comm,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(p * X).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case hba
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finset.range n).gcd p.coeff ∣ p.content

Tactic:
· exact Finset.gcd_mono (supp_subset_range h)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Tactic:
rw [← content_eq_zero_iff] at h

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ 1 * s.1.prod ∣ y

Tactic:
one_mul,

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑0! ∈ nonZeroDivisors R

Tactic:
simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ (p * ↑(normUnit p)).roots = p.roots

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ (↑(normUnit p) * p).roots = p.roots
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ p % q = p

Tactic:
mod_def,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ p %ₘ (q * C q.leadingCoeff⁻¹) = p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, ↑s = a.factors) ↔ a ≠ 0

Tactic:
← WithTop.ne_top_iff_exists

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors ≠ ⊤ ↔ a ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : p % q = p
⊢ p.degree < q.degree

Tactic:
mod_eq_self_iff hq0

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : p.degree < q.degree
⊢ p.degree < q.degree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
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
⊢ 1 * gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣ 1

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 * p.primPart).degree < ↑n

Tactic:
one_mul,

Goal state after:
case neg.inr
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
⊢ gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣ 1

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 * p.primPart).degree < ↑n
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).degree ≤ p.degree

Tactic:
mul_comm,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹) * C q.leadingCoeff⁻¹).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).degree < p.degree

Tactic:
mul_comm,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹) * C q.leadingCoeff⁻¹).degree < p.degree
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✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ←
    Multiset.map_replicate fun a => X - C a]
  rw [← Multiset.filter_eq]
  refine
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_
  convert! Polynomial.map_dvd f p.prod_multiset_X_sub_C_dvd
  simp only [Polynomial.map_multiset_prod, Multiset.map_map, Function.comp_apply,
    Polynomial.map_sub, map_X, map_C]

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 * p.primPart).degree < ↑n

Tactic:
mul_comm,

Goal state after:
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
⊢ (p.primPart * q.primPart.eraseLead).degree < ↑n
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
mod_def,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p %ₘ (q * C q.leadingCoeff⁻¹)) = map f p % map f q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p %ₘ (q * C q.leadingCoeff⁻¹)) = map f p % map f q

Tactic:
mod_def,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p %ₘ (q * C q.leadingCoeff⁻¹)) = map f p %ₘ (map f q * C (map f q).leadingCoeff⁻¹)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
mul_comm,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
mul_comm,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
⊢ r ∣ s.primPart

Tactic:
have h :=
      dvd_add rcs (Dvd.intro_left (C (leadingCoeff s) * X ^ (natDegree s - natDegree r)) rfl)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h✝ : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h✝
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
h :
  r ∣
    C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r +
      C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
⊢ r ∣ s.primPart
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}

Tactic:
rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]
  have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h
  simp [roots_C_mul_X_add_C _ this]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.degree = ↑0
⊢ ↑a.degree < ↑(a.degree + c.degree)

Tactic:
rw [Polynomial.degree_eq_natDegree cne0] at *

Goal state after:
case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬↑c.natDegree = ↑0
⊢ ↑a.degree < ↑(a.degree + ↑c.natDegree)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ q.leadingCoeff⁻¹ * p.leadingCoeff = p.leadingCoeff / q.leadingCoeff

pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Tactic:
mul_comm,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff⁻¹ = p.leadingCoeff / q.leadingCoeff

R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = 1 * (p * r)

Tactic:
one_mul,

Goal state after:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = p * r
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ C a.leadingCoeff * (a * C a.leadingCoeff⁻¹) = a

pp: case neg.h0
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0

Tactic:
mul_comm,

Goal state after:
case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a * C a.leadingCoeff⁻¹ * C a.leadingCoeff = a

case neg.h0
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a.leadingCoeff ≠ 0

case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0
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
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
a : A
x✝ : IsAlgebraic R (f a)
p : R[X]
hp0 : p ≠ 0
hp : (aeval (f a)) p = 0
⊢ f ((aeval a) p) = f 0

Tactic:
by rwa [map_zero, ← f.comp_apply, ← aeval_algHom]

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑g.symm = ↑g.symm ∘ₗ ↑f ∘ₗ a ∘ₗ ↑f.symm) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
← comp_assoc,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑g.symm = ((↑g.symm ∘ₗ ↑f) ∘ₗ a) ∘ₗ ↑f.symm) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : 0 - (aeval s) (C (q.coeff 0)) = (aeval s) (X * p)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
zero_sub,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : -(aeval s) (C (q.coeff 0)) = (aeval s) (X * p)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ 0 - (aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
zero_sub,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ -(aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / (0 - (algebraMap K L) (p.coeff 0))

Tactic:
zero_sub,

Goal state after:
case e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / -(algebraMap K L) (p.coeff 0)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) ((f y✝.fst j w✝¹) y✝.snd) = (f k i hki) ((f y✝.fst k w✝) y✝.snd)

Tactic:
map_map',

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f y✝.fst i ⋯) y✝.snd = (f k i hki) ((f y✝.fst k w✝) y✝.snd)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
⊢ { x // ∀ (i : ι) (hzi : z.fst ≤ i) (hwi : w.fst ≤ i), x = ih i ((f₁ z.fst i hzi) z.snd) ((f₂ w.fst i hwi) w.snd) }

Tactic:
choose j hzj hwj using exists_ge_ge z.1 w.1
  refine ⟨ih j (f₁ _ _ hzj z.2) (f₂ _ _ hwj w.2), fun k hzk hwk ↦ ?_⟩
  have ⟨i, hji, hki⟩ := exists_ge_ge j k
  simp_rw [compat _ _ hji, compat _ _ hki, map_map']

Goal state after: