mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

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

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

Tactic:
<;>

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

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

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

case imK
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ (↑(x * y)).imK = (↑x * ↑y).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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).re =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).re

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imI =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imI

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imJ =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imJ

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imK =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imK

Tactic:
<;>

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).re =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).re

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imI =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imI

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imJ =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imJ

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imK =
    ({ toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x).imK
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ ∀ {x : U}, IsIntegral R x ↔ ∃ y, (algebraMap S U) y = x

Tactic:
· intro x
    refine ⟨fun h ↦ ?_, ?_⟩
    · obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
      rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
      obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
      exact ⟨x, IsScalarTower.algebraMap_apply ..⟩
    · rintro ⟨x, rfl⟩
      rw [IsScalarTower.algebraMap_apply S T U]
      exact ((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

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

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

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

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

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₃]
⊢ { 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

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

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

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
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ Associated (a ^ n) (b ^ n) ↔ Associated a b

Tactic:
by
  simp_rw [← dvd_dvd_iff_associated, pow_dvd_pow_iff hn]

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₃]
⊢ 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

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₃]
⊢ 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)

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₃]
⊢ 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

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₃]
⊢ -(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)

Tactic:
<;>

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

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)

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

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

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

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

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

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₃]
⊢ { 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

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

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

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
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).re = (star b * star a).re

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imI = (star b * star a).imI

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imJ = (star b * star a).imJ

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imK = (star b * star a).imK

Tactic:
<;>

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).re = (star b * star a).re

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imI = (star b * star a).imI

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imJ = (star b * star a).imJ

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imK = (star b * star a).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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).re = (star a + star b).re

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imI = (star a + star b).imI

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imJ = (star a + star b).imJ

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imK = (star a + star b).imK

Tactic:
<;>

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).re = (star a + star b).re

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imI = (star a + star b).imI

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imJ = (star a + star b).imJ

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).imK = (star a + star b).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).re = (↑(2 * a.re + c₂ * a.imI)).re

pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imI = (↑(2 * a.re + c₂ * a.imI)).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imJ = (↑(2 * a.re + c₂ * a.imI)).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imK = (↑(2 * a.re + c₂ * a.imI)).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).re = (↑(2 * a.re + c₂ * a.imI)).re

case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imI = (↑(2 * a.re + c₂ * a.imI)).imI

case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imJ = (↑(2 * a.re + c₂ * a.imI)).imJ

case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a + star a).imK = (↑(2 * a.re + c₂ * a.imI)).imK
Module: Mathlib.Algebra.Quaternion

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

pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imI = (x * ↑r).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imJ = (x * ↑r).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imK = (x * ↑r).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).re = (x * ↑r).re

case imI
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imI = (x * ↑r).imI

case imJ
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imJ = (x * ↑r).imJ

case imK
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r * x).imK = (x * ↑r).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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).re = (a * (↑(2 * a.re + c₂ * a.imI) - a)).re

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imI = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imI

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imJ = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imJ

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imK = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imK

Tactic:
<;>

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).re = (a * (↑(2 * a.re + c₂ * a.imI) - a)).re

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imI = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imI

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imJ = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imJ

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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imK = (a * (↑(2 * a.re + c₂ * a.imI) - a)).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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
<;>

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)

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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)
Module: Mathlib.Algebra.Quaternion

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

pp: case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imI = (↑x).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imJ = (↑x).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imK = (↑x).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).re = (↑x).re

case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imI = (↑x).imI

case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imJ = (↑x).imJ

case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imK = (↑x).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).re = (-a.im + ↑c₂ * ↑a.imI).re

pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imI = (-a.im + ↑c₂ * ↑a.imI).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imJ = (-a.im + ↑c₂ * ↑a.imI).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imK = (-a.im + ↑c₂ * ↑a.imI).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).re = (-a.im + ↑c₂ * ↑a.imI).re

case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imI = (-a.im + ↑c₂ * ↑a.imI).imI

case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imJ = (-a.im + ↑c₂ * ↑a.imI).imJ

case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a.im).imK = (-a.im + ↑c₂ * ↑a.imI).imK