mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : AddGroup 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✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b), (equivProd a b) (-x) = -(equivProd a b) x

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x - y) = (equivProd a b) x - (equivProd a b) y

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

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

case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x - y) = (equivProd a b) x - (equivProd a b) y

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

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

pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ - y✝) = (equivProd a b) x✝ - (equivProd a b) y✝

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

pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup 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✝ : AddGroup 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✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (-x✝) = -(equivProd a b) x✝

case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ - y✝) = (equivProd a b) x✝ - (equivProd a b) y✝

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

case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup 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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑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✝ : AddCommMonoidWithOne R
⊢ (QuadraticAlgebra.C ↑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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).re = (QuadraticAlgebra.C ↑n + 1).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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).im = (QuadraticAlgebra.C ↑n + 1).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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).re = (QuadraticAlgebra.C ↑n + 1).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✝ : AddCommMonoidWithOne R
n : ℕ
⊢ (QuadraticAlgebra.C ↑(n + 1)).im = (QuadraticAlgebra.C ↑n + 1).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).re = (OfNat.ofNat n).re

pp: case im
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).im = (OfNat.ofNat n).im

Tactic:
<;>

Goal state after:
case re
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).re = (OfNat.ofNat n).re

case im
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).im = (OfNat.ofNat n).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✝ : NonUnitalNonAssocSemiring R
x✝² 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✝ : NonUnitalNonAssocSemiring R
x✝² 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✝ : NonUnitalNonAssocSemiring R
x✝² 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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * (x✝¹ + x✝)).im = (x✝² * 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✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝².re * x✝¹.re + x✝².re * x✝.re + (a * x✝².im * x✝¹.im + a * x✝².im * x✝.im) =
    x✝².re * x✝¹.re + a * x✝².im * x✝¹.im + (x✝².re * x✝.re + a * x✝².im * x✝.im)

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

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

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

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

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

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

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

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

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

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

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

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✝ : NonAssocSemiring 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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (1 * x✝).im = 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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).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✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ (x✝ * 1).im = x✝.im
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

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

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

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

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

Tactic:
<;>

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

case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ ({ re := x, im := y } * star { re := x, im := y }).im =
    ((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).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✝ : CommSemiring R
x✝² x✝¹ 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✝ : CommSemiring R
x✝² x✝¹ 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✝ : CommSemiring R
x✝² x✝¹ 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✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹ * x✝).im = (x✝² * (x✝¹ * x✝)).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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

pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 0

Tactic:
<;>

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

case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 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✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.re +
      a * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) + a * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)

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

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✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.im + (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.re +
      b * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im) + x✝².im * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) +
      b * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).re = (star b * star a).re

pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).im = (star b * star a).im

Tactic:
<;>

Goal state after:
case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).re = (star b * star a).re

case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : CommRing R
a b : QuadraticAlgebra R a✝ b✝
⊢ (star (a * b)).im = (star b * star a).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✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).re = (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✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).im = (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✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).re = (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✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).im = (x✝ * x✝¹).im