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

Goal state before:
pp: case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imJ = (-↑x).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imK = (-↑x).imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
⊢ ↑↑0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
⊢ ∀ (n : ℕ), ↑↑(n + 1) = ↑↑n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * x✝)).re

Tactic:
simp

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.re +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imI +
          c₃ *
              (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
                c₁ * x✝².imK * x✝¹.imI) *
            x✝.imJ +
        c₂ * c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK -
      c₁ * c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imK =
    x✝².re *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
          c₃ * x✝².imJ *
            (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
              c₁ * x✝¹.imK * x✝.imI) +
        c₂ * c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
      c₁ * c₃ * x✝².imK *
        (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imI = (x✝² * (x✝¹ * x✝)).imI

Tactic:
simp

Goal state after:
case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imI +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.re +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imI -
        c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK +
      c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imJ =
    x✝².re *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
            x✝².imI *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
              c₃ * x✝¹.imK * x✝.imJ) -
        c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
      c₃ * x✝².imK *
        (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imJ = (x✝² * (x✝¹ * x✝)).imJ

Tactic:
simp

Goal state after:
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imJ +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imK +
          (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
            x✝.re +
        c₂ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI -
      c₁ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imI =
    x✝².re *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
          x✝².imJ *
            (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
              c₁ * c₃ * x✝¹.imK * x✝.imK) +
        c₂ * x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) -
      c₁ * x✝².imK *
        (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imK = (x✝² * (x✝¹ * x✝)).imK

Tactic:
simp

Goal state after:
case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imK +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imJ +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imK -
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
            c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI +
      (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.re =
    x✝².re * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
            x✝².imI *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
        x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) +
      x✝².imK *
        (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
          c₁ * c₃ * x✝¹.imK * x✝.imK)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).re = x✝.re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imI = x✝.imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imJ = x✝.imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imK = x✝.imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).re = x✝.re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imI = x✝.imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imJ = x✝.imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imK = x✝.imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).re = re 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imI = imI 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imJ = imJ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imK = imK 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).re = re 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imI = imI 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imJ = imJ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imK = imK 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * x✝).re

Tactic:
simp

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.re + x✝.re) + c₁ * x✝².imI * (x✝¹.imI + x✝.imI) + c₃ * x✝².imJ * (x✝¹.imJ + x✝.imJ) +
        c₂ * c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) -
      c₁ * c₃ * x✝².imK * (x✝¹.imK + x✝.imK) =
    x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
        c₁ * c₃ * x✝².imK * x✝¹.imK +
      (x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imI = (x✝² * x✝¹ + x✝² * x✝).imI

Tactic:
simp

Goal state after:
case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imI + x✝.imI) + x✝².imI * (x✝¹.re + x✝.re) + c₂ * x✝².imI * (x✝¹.imI + x✝.imI) -
        c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) +
      c₃ * x✝².imK * (x✝¹.imJ + x✝.imJ) =
    x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK + c₃ * x✝².imK * x✝¹.imJ +
      (x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imJ = (x✝² * x✝¹ + x✝² * x✝).imJ

Tactic:
simp

Goal state after:
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imJ + x✝.imJ) + c₁ * x✝².imI * (x✝¹.imK + x✝.imK) + x✝².imJ * (x✝¹.re + x✝.re) +
        c₂ * x✝².imJ * (x✝¹.imI + x✝.imI) -
      c₁ * x✝².imK * (x✝¹.imI + x✝.imI) =
    x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI - c₁ * x✝².imK * x✝¹.imI +
      (x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imK = (x✝² * x✝¹ + x✝² * x✝).imK

Tactic:
simp

Goal state after:
case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imK + x✝.imK) + x✝².imI * (x✝¹.imJ + x✝.imJ) + c₂ * x✝².imI * (x✝¹.imK + x✝.imK) -
        x✝².imJ * (x✝¹.imI + x✝.imI) +
      x✝².imK * (x✝¹.re + x✝.re) =
    x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re +
      (x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).re = (x✝² * x✝ + x✝¹ * x✝).re

Tactic:
simp

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imJ +
        c₂ * c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK -
      c₁ * c₃ * (x✝².imK + x✝¹.imK) * x✝.imK =
    x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK +
      (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
        c₁ * c₃ * x✝¹.imK * x✝.imK)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imI = (x✝² * x✝ + x✝¹ * x✝).imI

Tactic:
simp

Goal state after:
case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re + c₂ * (x✝².imI + x✝¹.imI) * x✝.imI -
        c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₃ * (x✝².imK + x✝¹.imK) * x✝.imJ =
    x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ +
      (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imJ = (x✝² * x✝ + x✝¹ * x✝).imJ

Tactic:
simp

Goal state after:
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re +
        c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imI -
      c₁ * (x✝².imK + x✝¹.imK) * x✝.imI =
    x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI +
      (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imK = (x✝² * x✝ + x✝¹ * x✝).imK

Tactic:
simp

Goal state after:
case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ + c₂ * (x✝².imI + x✝¹.imI) * x✝.imK -
        (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : f (eval y (p.scaleRoots x)) = 0
⊢ (p.scaleRoots x).IsRoot y

Tactic:
hf

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval y (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ (↑(x * y)).re = (↑x * ↑y).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ (↑(x * y)).imI = (↑x * ↑y).imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ (↑(x * y)).imJ = (↑x * ↑y).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ (↑(x * y)).imK = (↑x * ↑y).imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₃]
⊢ (fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK })
      ((fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }) x✝) =
    x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₃,c₁]
⊢ (fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK })
      ((fun t ↦ { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }) x✝) =
    x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK }.re =
    ({ re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
        { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }).re

Tactic:
simp

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ - c₁ * c₃ * x✝¹.imK * x✝.imK =
    x✝¹.re * x✝.re + c₃ * x✝¹.imJ * x✝.imJ + c₁ * x✝¹.imI * x✝.imI - c₃ * c₁ * x✝¹.imK * x✝.imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK }.imI =
    ({ re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
        { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }).imI

Tactic:
simp

Goal state after:
case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI =
    x✝¹.re * x✝.imJ + x✝¹.imJ * x✝.re + c₁ * x✝¹.imI * x✝.imK + -(c₁ * x✝¹.imK * x✝.imI)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK }.imJ =
    ({ re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
        { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }).imJ

Tactic:
simp

Goal state after:
case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₃ * x✝¹.imJ * x✝.imK =
    x✝¹.re * x✝.imI + -(c₃ * x✝¹.imJ * x✝.imK) + x✝¹.imI * x✝.re
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK }.imK =
    ({ re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
        { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }).imK

Tactic:
simp

Goal state after:
case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ -(x✝¹.imK * x✝.re) + (x✝¹.imJ * x✝.imI - (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ)) =
    -(x✝¹.re * x✝.imK) + x✝¹.imJ * x✝.imI - x✝¹.imI * x✝.imJ + -(x✝¹.imK * x✝.re)