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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i Df + i Dg = i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)

Tactic:
Hf,

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i Dg =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
by_cases h2 : p.natDegree < n
  · rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
    by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
    · rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
      grw [h2, add_tsub_cancel_left]
    · rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
  rw [not_lt] at h2
  rw [revAt_le (h2.trans (Nat.le_add_right _ _))]
  by_cases h3 : p.natTrailingDegree ≤ n
  · rw [← tsub_add_eq_add_tsub h2, ← tsub_tsub_assoc h2 h3, mirror, coeff_mul_X_pow', if_pos h3,
      coeff_reverse, revAt_le (tsub_le_self.trans h2)]
  rw [not_le] at h3
  rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]
  exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * h * (g.mirror * h.mirror) = k * (g.mirror * h)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * (h * (g.mirror * h.mirror)) = k * (g.mirror * h)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * (h.mirror * g.mirror * h) = k * (g.mirror * h)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * (h.mirror * (g.mirror * h)) = k * (g.mirror * h)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

pp: case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0

Tactic:
· aesop (add simp coeff_monomial)

Goal state after:
case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ p.smeval x = p.sum (smul_pow x)

Tactic:
by rw [smeval_def]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun e a ↦ RingHom.smulOneHom a * x ^ e) = p.sum (smul_pow x)

Tactic:
congr 1 with e a

Goal state after:
case e_f
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
e : ℕ
a : R
⊢ RingHom.smulOneHom a * x ^ e = smul_pow x e a
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ 1 * X ^ n * p).smeval x = x ^ (1 + n) * p.smeval x

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ 1 * (X ^ n * p)).smeval x = x ^ (1 + n) * p.smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ ((monomial n) r✝ * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ (C r✝ * X ^ n * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ (C r✝ * X ^ n * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))

Tactic:
mul_assoc,

Goal state after:
case add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ (C r✝ * (X ^ n * (r + s))).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ n * x * q.smeval y = x ^ n * q.smeval y * x

Tactic:
mul_assoc,

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ n * (x * q.smeval y) = x ^ n * q.smeval y * x
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r
      (∑ x ∈ range k.succ,
        (X - C r) ^ 1 * (k.choose x * q.descFactorial (k - x)) • (X - C r) ^ (q - (k - x) - 1) * (⇑derivative)^[x] p') =
    0

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r
      (∑ x ∈ range k.succ,
        (X - C r) ^ 1 *
          ((k.choose x * q.descFactorial (k - x)) • (X - C r) ^ (q - (k - x) - 1) * (⇑derivative)^[x] p')) =
    0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * X ^ (n - k) * X ^ k + C v * X ^ (n - m) * X ^ k + C w * X ^ (n - n) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * (X ^ (n - k) * X ^ k) + C v * X ^ (n - m) * X ^ k + C w * X ^ (n - n) * X ^ k = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * (X ^ (n - k) * X ^ k) + C v * X ^ (n - m) * X ^ k + C w * X ^ (n - n) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * (X ^ (n - k) * X ^ k) + C v * (X ^ (n - m) * X ^ k) + C w * X ^ (n - n) * X ^ k =
    trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * (X ^ (n - k) * X ^ k) + C v * (X ^ (n - m) * X ^ k) + C w * X ^ (n - n) * X ^ k =
    trinomial k (n - m + k) n w v u

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * (X ^ (n - k) * X ^ k) + C v * (X ^ (n - m) * X ^ k) + C w * (X ^ (n - n) * X ^ k) =
    trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k k✝ n ↑u ↑v ↑w).coeff k✝)

Tactic:
refine ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * b j * g j + r j * a j * g i

Tactic:
mul_assoc,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * (b j * g j) + r j * a j * g i
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * (b j * g j) + r j * a j * g i

Tactic:
mul_assoc,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * (b j * g j) + r j * (a j * g i)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < η * P.coeff (d + 1)

Tactic:
trans 0

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < 0

R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ 0 < η * P.coeff (d + 1)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul :
  ↑w * (trinomial k m n ↑u ↑v ↑w).trailingCoeff =
    (trinomial k m' n ↑x ↑v ↑z).leadingCoeff * (trinomial k m' n ↑x ↑v ↑z).trailingCoeff
⊢ q = p ∨ q = p.mirror

Tactic:
trinomial_leadingCoeff hkm' hmn' z.ne_zero,

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * (trinomial k m n ↑u ↑v ↑w).trailingCoeff = ↑z * (trinomial k m' n ↑x ↑v ↑z).trailingCoeff
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * ↑w * ↑u + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror

Tactic:
mul_assoc,

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * (↑w * ↑u) + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ s • x =
    { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s *
      x

Tactic:
by ext <;> simp [Algebra.smul_def]

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

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * star x * (algebraMap R (QuadraticAlgebra R a b)) r = (algebraMap R (QuadraticAlgebra R a b)) 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
mul_assoc,

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * (star x * (algebraMap R (QuadraticAlgebra R a b)) r) = (algebraMap R (QuadraticAlgebra R a b)) 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ ((algebraMap R[X] K) q * ∏ x ∈ s, (algebraMap R[X] K) (g x ^ n x)) * ∏ i ∈ s, gi i ^ n i +
      (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ (algebraMap R[X] K) q * ((∏ x ∈ s, (algebraMap R[X] K) (g x ^ n x)) * ∏ i ∈ s, gi i ^ n i) +
      (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i *
      (((algebraMap R[X] K) (r i j.rev * g i ^ ↑j.rev) * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x ^ n x)) *
        ∏ x ∈ s.erase i, gi x ^ n x) =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i *
      ((algebraMap R[X] K) (r i j.rev * g i ^ ↑j.rev) *
        ((∏ x ∈ s.erase i, (algebraMap R[X] K) (g x ^ n x)) * ∏ x ∈ s.erase i, gi x ^ n x)) =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * q.i = -c₁ • q.j

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * (q.j * q.i) = -c₁ • q.j
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * q.j = c₃ • q.i

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * (q.j * q.j) = c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.j * (q.i * q.j) = -((c₁ * c₃) • 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * (q.j * (q.i * q.j)) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * q.j * q.j) - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * (q.j * q.j)) - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)