mathlib-initiative/mathlib-tactics huggingface dataset:
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'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r ((⇑derivative)^[q] (map (algebraMap R A) p)) = q ! • eval r p'

Tactic:
simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul]

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'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ x ∈ range q.succ, (q.choose x * q.descFactorial (q - x)) • (X - C r) ^ (q - (q - x)) * (⇑derivative)^[x] p') =
    q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.zero
⊢ SignType.zero = -SignType.sign P.eraseLead.leadingCoeff

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.neg
⊢ SignType.neg = -SignType.sign P.eraseLead.leadingCoeff

pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.pos
⊢ SignType.pos = -SignType.sign P.eraseLead.leadingCoeff

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.zero
⊢ SignType.zero = -SignType.sign P.eraseLead.leadingCoeff

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.neg
⊢ SignType.neg = -SignType.sign P.eraseLead.leadingCoeff

case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.pos
⊢ SignType.pos = -SignType.sign P.eraseLead.leadingCoeff
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ ∑ x ∈ range (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)

Tactic:
simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]

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

Goal state before:
pp: case h.left
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 + n

pp: case h.right
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 < n + n

Tactic:
<;>

Goal state after:
case h.left
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 + n

case h.right
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 < n + n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
p q : ℤ[X]
k m' n : ℕ
hkm' : k < m'
hmn' : m' < n
u v : ℤˣ
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
hq : q = trinomial k m' n ↑u ↑v ↑u
hkm : k < n - m' + k
hmn : n - m' + k < n
hp : trinomial k m' n ↑u ↑v ↑u = p.mirror
h : n - (n - m' + k) + k = m'
⊢ q = p.mirror

Tactic:
exact hq.trans hp

Goal state after:
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

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:
<;>

Goal state after:
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

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
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

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

Tactic:
<;>

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

case im
R : Type u_1
a b : R
inst✝ : NegZeroClass R
x : R
⊢ (QuadraticAlgebra.C (-x)).im = (-QuadraticAlgebra.C x).im
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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).re = (s • t • z).re

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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).im = (s • t • z).im

Tactic:
<;>

Goal state after:
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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).re = (s • t • z).re

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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ ((s • t) • z).im = (s • t • z).im
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✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).re = (t • s • z).re

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✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).im = (t • s • z).im

Tactic:
<;>

Goal state after:
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✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).re = (t • s • z).re

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✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
z : QuadraticAlgebra R a b
⊢ (s • t • z).im = (t • s • z).im
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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).re = (s • z).re

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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).im = (s • z).im

Tactic:
<;>

Goal state after:
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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).re = (s • z).re

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✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
s : S
z : QuadraticAlgebra R a b
⊢ (MulOpposite.op s • z).im = (s • z).im
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✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).re = (x✝² • x✝¹ • x✝).re

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✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).im = (x✝² • x✝¹ • x✝).im

Tactic:
<;>

Goal state after:
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✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).re = (x✝² • x✝¹ • x✝).re

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✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ ((x✝² * x✝¹) • x✝).im = (x✝² • x✝¹ • x✝).im
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
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

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:
<;>

Goal state after:
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

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
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

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:
<;>

Goal state after:
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

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
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

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

Tactic:
<;>

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

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = { re := a, im := b }.im
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

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

Tactic:
<;>

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

case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ (ω * ω).im = (a • 1 + b • ω).im
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

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:
<;>

Goal state after:
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

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
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
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
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).re = (r • x + s • x).re

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
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
<;>

Goal state after:
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
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).re = (r • x + s • x).re

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
r s : S
x : QuadraticAlgebra R a b
⊢ ((r + s) • x).im = (r • x + s • x).im
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

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:
<;>

Goal state after:
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

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