mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ f i * ((Multiset.map f (s.erase j)).prod * derivative (f j)) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)

Tactic:
← mul_assoc,

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ f i * (Multiset.map f (s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod * (c * k) = x * (y * k)

Tactic:
← mul_assoc,

Goal state after:
case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod * c * k = x * (y * k)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod * c * k = x * (y * k)

Tactic:
← mul_assoc,

Goal state after:
case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod * c * k = x * y * k
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod

Goal state after:
case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (x * c)
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a * s.prod ∣ n

Tactic:
obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)

Goal state after:
case cons
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
⊢ a * s.prod ∣ a * k
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
← mul_assoc,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (C r * X ^ k).content r

Tactic:
associated_content_C_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Associated (r * (X ^ k).content) r
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
Finset.dvd_gcd_iff

Goal state after:
case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∀ b ∈ Finset.range n, p.content ∣ p.coeff b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ (Multiset.map (⇑e) w).prod * ↑((Units.map e.toMonoidHom) u) = a

Tactic:
Multiset.prod_hom,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * ↑((Units.map e.toMonoidHom) u) = a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.support.gcd p.coeff

Tactic:
Finset.dvd_gcd_iff

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
by
    rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ¬∃ a ∈ a✝, ↑a = 0

Tactic:
not_exists

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ ↑u * (C ↑w⁻¹ * C ↑(normUnit a✝.leadingCoeff)) = C ↑(normUnit a✝.leadingCoeff)

Tactic:
← mul_assoc,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ ↑u * C ↑w⁻¹ * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (C p.content * (p.primPart * (C q.content * q.primPart))).content
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)

Tactic:
associated_content_C_mul,

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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (p.primPart * (C q.content * q.primPart)).content)
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (p.primPart * (C q.content * q.primPart)).content)
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)

Tactic:
associated_content_C_mul,

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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (p.primPart * (C q.content * q.primPart)).content)
    (p.content * p.primPart.content * (C q.content * q.primPart).content)
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (C q.content * (q.primPart * p.primPart)).content)
    (p.content * p.primPart.content * (C q.content * q.primPart).content)

Tactic:
associated_content_C_mul,

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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * (q.primPart * p.primPart).content))
    (p.content * p.primPart.content * (C q.content * q.primPart).content)
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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * (q.primPart * p.primPart).content))
    (p.content * p.primPart.content * (C q.content * q.primPart).content)

Tactic:
associated_content_C_mul,

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
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * (q.primPart * p.primPart).content))
    (p.content * p.primPart.content * (q.content * q.primPart.content))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
⊢ p ∣ Associates.mk a

Tactic:
by
  have := Classical.decEq (Associates α)
  apply dvd_of_mem_factors
  rw [factors_mk _ hz]
  apply mem_factorSet_some.2 h_mem

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]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ ∃ r, r.IsPrimitive ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s

Tactic:
have h : ∃ (n : ℕ) (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r :=
      ⟨(p * q).natDegree, p * q, rfl, hp.mul hq, dvd_mul_right _ _, dvd_mul_left _ _⟩

Goal state after:
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.IsPrimitive ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
⊢ False

Tactic:
obtain ⟨p, hp, hpa, hpb⟩ := exists_prime_dvd_of_not_inf_one ha0 hb0 hg

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
p : α
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
← mul_assoc,

Goal state after:
case e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a * C a⁻¹ * (q * C q.leadingCoeff⁻¹) = q * C q.leadingCoeff⁻¹
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 = C a * (C a⁻¹ * (p * r))

Tactic:
← mul_assoc,

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 = C a * C a⁻¹ * (p * r)
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 ∣ C a * q
r : R[X]
hr : C a * q = p * r
⊢ q = C a⁻¹ * (C a * q)

Tactic:
← mul_assoc,

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
w : Multiset (MvPolynomial (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial (↥s) D)ˣ
hw : w.prod * ↑u = a'
⊢ (Multiset.map (⇑(rename Subtype.val)) w).prod * ↑((Units.map ↑(rename Subtype.val).toRingHom) u) =
    (rename Subtype.val) a'

Tactic:
Multiset.prod_hom,

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
w : Multiset (MvPolynomial (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial (↥s) D)ˣ
hw : w.prod * ↑u = a'
⊢ (rename Subtype.val) w.prod * ↑((Units.map ↑(rename Subtype.val).toRingHom) u) = (rename Subtype.val) a'
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

Tactic:
map_add,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X) + (aeval x) (C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: 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
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) (p.divX * X + C (p.coeff 0))

Tactic:
map_add,

Goal state after:
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
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) (p.divX * X) + (aeval x) (C (p.coeff 0))
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
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 : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
x y z : DirectLimit F f
⊢ C x y z

Tactic:
obtain ⟨_, _, _, _, rfl, rfl, rfl⟩ := exists_eq_mk₃ f x y z

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
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 : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
w✝³ : ι
w✝² w✝¹ w✝ : F w✝³
⊢ C ⟦⟨w✝³, w✝²⟩⟧ ⟦⟨w✝³, w✝¹⟩⟧ ⟦⟨w✝³, w✝⟩⟧
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i ↦ G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x + (f j k hjk) y) = Quotient.mk'' (p + q)

Tactic:
map_add,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i ↦ G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x) + (of R ι G f k) ((f j k hjk) y) = Quotient.mk'' (p + q)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 = 0

Tactic:
simp only [map_zero]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 = 0

Tactic:
simp only [map_zero]

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 : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ 1 * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [one_def i, mul_def, one_mul]

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
nontriviality R; exact eq_of_smul_eq_smul

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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
z : ℤ
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ ^ z) = DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ ^ z

Tactic:
simp_rw [zpow₀_def, lift_def, map_zpow₀ (g i)]

Goal state after: