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

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + 0 +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
Finsupp.filter_single_of_neg,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + 0 +
              (0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + 0 +
              (0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
Finsupp.filter_single_of_neg,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + 0 +
              (0 + 0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + n ∉ Set.Ioo (k + n) (n + n)

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : q ≤ k
⊢ ⋯.choose.natDegree ≤ p.natDegree - k

pp: case neg
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : ¬q ≤ k
⊢ natDegree 0 ≤ p.natDegree - k

Tactic:
· exact (aeval_iterate_derivative_of_ge A p q h).choose_spec.1

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : ¬q ≤ k
⊢ natDegree 0 ≤ p.natDegree - k
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ -(η * c) = (X - C η).coeff 0 * c

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ ∀ b ∈ s, ((r₁ b - r₂ b) * ∏ k ∈ s.erase b, g k).degree < (∏ i ∈ s, g i).degree

Tactic:
intro j

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
⊢ j ∈ s → ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < (∏ i ∈ s, g i).degree
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : AddZeroClass R
x y : R
⊢ (QuadraticAlgebra.C (x + y)).re = (QuadraticAlgebra.C x + QuadraticAlgebra.C y).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : AddZeroClass R
x y : R
⊢ (QuadraticAlgebra.C (x + y)).im = (QuadraticAlgebra.C x + QuadraticAlgebra.C y).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : NegZeroClass R
x : R
⊢ (QuadraticAlgebra.C (-x)).re = (-QuadraticAlgebra.C x).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : NegZeroClass R
x : R
⊢ (QuadraticAlgebra.C (-x)).im = (-QuadraticAlgebra.C x).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝ : QuadraticAlgebra R a b
⊢ (1 • x✝).re = x✝.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝ : QuadraticAlgebra R a b
⊢ (1 • x✝).im = x✝.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝ : S
⊢ (x✝ • 0).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝ : S
⊢ (x✝ • 0).im = im 0

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² • (x✝¹ + x✝)).re = (x✝² • x✝¹ + x✝² • x✝).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² • (x✝¹ + x✝)).im = (x✝² • x✝¹ + x✝² • x✝).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).re = { re := a, im := b }.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = { re := a, im := b }.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).re = (a • 1 + b • ω).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = (a • 1 + b • ω).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ (ω * { re := x, im := y }).re = { re := a * y, im := x + b * y }.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ (ω * { re := x, im := y }).im = { re := a * y, im := x + b * y }.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ (ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y }).re =
    { re := a * n * y, im := n * x + n * b * y }.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ (ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y }).im =
    { re := a * n * y, im := n * x + n * b * y }.im

Tactic:
simp

Goal state after:
case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ n * x + b * n * y = n * x + n * b * y
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y }.re = ((algebraMap R (QuadraticAlgebra R a b)) x + y • ω).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y }.im = ((algebraMap R (QuadraticAlgebra R a b)) x + y • ω).im

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
⊢ re 1 • 1 + im 1 • ↑u = 1

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ (0 • x).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ (0 • x).im = im 0

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑0).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑0).im = im 0

Tactic:
simp

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

Goal state before:
pp: case isTrue.isTrue.nil
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs✝ : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
hcs : List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs) = []
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1 []).length ≤
    (1 :: List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀) []).length

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).re = (QuadraticAlgebra.C ↑n + 1).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).im = (QuadraticAlgebra.C ↑n + 1).im

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re * w.re + a * z.im * w.im) • 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • ↑u =
    (z * w).re • 1 + (z * w).im • ↑u

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
⊢ re 0 • 1 + im 0 • ↑u = 0

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (0 * x✝).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (0 * x✝).im = im 0

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 0).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 0).im = im 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
r : { u // u * u = a • 1 + b • u }
⊢ (fun f ↦ ⟨f ω, ⋯⟩)
      ((fun u ↦
          { toFun := fun z ↦ z.re • 1 + z.im • ↑u, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
            commutes' := ⋯ })
        r) =
    r

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ (QuadraticAlgebra.C r * x).re = (r • x).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ (QuadraticAlgebra.C r * x).im = (r • x).im

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : QuadraticAlgebra R a b →ₐ[R] A
⊢ ((fun u ↦
          { toFun := fun z ↦ z.re • 1 + z.im • ↑u, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
            commutes' := ⋯ })
        ((fun f ↦ ⟨f ω, ⋯⟩) f))
      ω =
    f ω

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (QuadraticAlgebra.C (x * y)).re = (QuadraticAlgebra.C x * QuadraticAlgebra.C y).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (QuadraticAlgebra.C (x * y)).im = (QuadraticAlgebra.C x * QuadraticAlgebra.C y).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (1 * x✝).re = x✝.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (1 * x✝).im = x✝.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).re = x✝.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).im = x✝.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ ({ re := x, im := y } * star { re := x, im := y }).re =
    ((algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
          (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
            (algebraMap R (QuadraticAlgebra R a b)) y -
        (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
          (algebraMap R (QuadraticAlgebra R a b)) y).re

Tactic:
simp

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ x * (x + b * y) + -(a * y * y) = x * x + b * x * y - a * y * y