[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₁ q₂ : Basis A c₁ c₂
hi : q₁.i = q₂.i
hj : q₁.j = q₂.j
⊢ q₁ = q₂
[PROOFSTEP]
cases q₁
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₂ : Basis A c₁ c₂
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i =
    q₂.i
hj :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j =
    q₂.j
⊢ { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ } = q₂
[PROOFSTEP]
rename_i q₁_i_mul_j _
[GOAL]
case mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q₂ : Basis A c₁ c₂
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₁_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝ }.i =
    q₂.i
hj :
  { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝ }.j =
    q₂.j
⊢ { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₁_i_mul_j, j_mul_i := j_mul_i✝ } =
    q₂
[PROOFSTEP]
cases q₂
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }
[PROOFSTEP]
rename_i q₂_i_mul_j _
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j, j_mul_i := j_mul_i✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_k
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ k✝¹ = k✝
[PROOFSTEP]
rw [← q₁_i_mul_j, ← q₂_i_mul_j]
[GOAL]
case mk.mk.e_k
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1
j_mul_j✝¹ : j✝¹ * j✝¹ = c₂ • 1
q₁_i_mul_j : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = -k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1
j_mul_j✝ : j✝ * j✝ = c₂ • 1
q₂_i_mul_j : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = -k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := q₁_i_mul_j,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := q₂_i_mul_j,
        j_mul_i := j_mul_i✝ }.j
⊢ i✝¹ * j✝¹ = i✝ * j✝
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } = c₁ • 1
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re = (c₁ • 1).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI = (c₁ • 1).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ = (c₁ • 1).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK = (c₁ • 1).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } = c₂ • 1
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re = (c₂ • 1).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI = (c₂ • 1).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ = (c₂ • 1).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK = (c₂ • 1).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    -{ re := 0, imI := 0, imJ := 0, imK := 1 }
[PROOFSTEP]
ext
[GOAL]
case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).re
[PROOFSTEP]
simp
[GOAL]
case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imI
[PROOFSTEP]
simp
[GOAL]
case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imJ
[PROOFSTEP]
simp
[GOAL]
case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK =
    (-{ re := 0, imI := 0, imJ := 0, imK := 1 }).imK
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.i * q.k = c₁ • q.j
[PROOFSTEP]
rw [← i_mul_j, ← mul_assoc, i_mul_i, smul_mul_assoc, one_mul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.i = -c₁ • q.j
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, j_mul_i, mul_neg, i_mul_k, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.j = c₂ • q.i
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.j * q.k = -c₂ • q.i
[PROOFSTEP]
rw [← i_mul_j, ← mul_assoc, j_mul_i, neg_mul, k_mul_j, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.k * q.k = -((c₁ * c₂) • 1)
[PROOFSTEP]
rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_neg, ← mul_assoc, i_mul_i,
  smul_mul_assoc, one_mul, neg_mul, smul_mul_assoc, j_mul_j, smul_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ lift q 0 = 0
[PROOFSTEP]
simp [lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ lift q 1 = 1
[PROOFSTEP]
simp [lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ lift q (x + y) = lift q x + lift q y
[PROOFSTEP]
simp [lift, add_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ lift q (x * y) = lift q x * lift q y
[PROOFSTEP]
simp only [lift, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re • 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
[PROOFSTEP]
simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) +
            (x.imI * y.imK) • (q.i * q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) +
          (x.imJ * y.imK) • (q.j * q.k)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) +
        (x.imK * y.imK) • (q.k * q.k))
[PROOFSTEP]
simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • c₁ • 1 + (x.imI * y.imJ) • q.k + (x.imI * y.imK) • c₁ • q.j) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • -q.k + (x.imJ * y.imJ) • c₂ • 1 + (x.imJ * y.imK) • -c₂ • q.i) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₂ • q.i +
        (x.imK * y.imK) • -((c₁ * c₂) • 1))
[PROOFSTEP]
simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ← add_assoc, mul_neg, neg_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI * c₁) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK * c₁) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((x.imK * y.imK * (c₁ * c₂)) • 1)
[PROOFSTEP]
simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI * c₁) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK * c₁) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((c₁ * c₂ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [mul_comm _ c₁, mul_right_comm _ _ c₁]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * (x.imI * y.imI)) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * (x.imI * y.imK)) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (x.imJ * y.imJ * c₂) • 1 +
              -((x.imJ * y.imK * c₂) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * y.imJ * c₂) • q.i +
      -((c₁ * c₂ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [mul_comm _ c₂, mul_right_comm _ _ c₂]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * (x.imI * y.imI)) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * (x.imI * y.imK)) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * (x.imJ * y.imJ)) • 1 +
              -((c₂ * (x.imJ * y.imK)) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (c₂ * (x.imK * y.imJ)) • q.i +
      -((c₂ * c₁ * (x.imK * y.imK)) • 1)
[PROOFSTEP]
simp only [← mul_comm c₁ c₂, ← mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
simp [sub_eq_add_neg, add_smul, ← add_assoc]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₂ * x.imJ * y.imJ) • 1 + -((c₁ * c₂ * x.imK * y.imK) • 1) +
                            (x.re * y.imI) • q.i +
                          (x.imI * y.re) • q.i +
                        -((c₂ * x.imJ * y.imK) • q.i) +
                      (c₂ * x.imK * y.imJ) • q.i +
                    (x.re * y.imJ) • q.j +
                  (c₁ * x.imI * y.imK) • q.j +
                (x.imJ * y.re) • q.j +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.re * y.imK) • q.k +
          (x.imI * y.imJ) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₂ * x.imJ * y.imJ) • 1 + -((c₁ * c₂ * x.imK * y.imK) • 1) +
                            (x.re * y.imI) • q.i +
                          (x.imI * y.re) • q.i +
                        -((c₂ * x.imJ * y.imK) • q.i) +
                      (c₂ * x.imK * y.imJ) • q.i +
                    (x.re * y.imJ) • q.j +
                  (c₁ * x.imI * y.imK) • q.j +
                (x.imJ * y.re) • q.j +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.re * y.imK) • q.k +
          (x.imI * y.imJ) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (c₁ * x.imI * y.imI) • 1 +
                        (x.imI * y.imJ) • q.k +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  -((x.imJ * y.imI) • q.k) +
                (c₂ * x.imJ * y.imJ) • 1 +
              -((c₂ * x.imJ * y.imK) • q.i) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (c₂ * x.imK * y.imJ) • q.i +
      -((c₁ * c₂ * x.imK * y.imK) • 1)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
r : R
x : ℍ[R,c₁,c₂]
⊢ lift q (r • x) = r • lift q x
[PROOFSTEP]
simp [lift, mul_smul, ← Algebra.smul_def]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.i * ↑F q.i = c₁ • 1
[PROOFSTEP]
rw [← F.map_mul, q.i_mul_i, F.map_smul, F.map_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.j * ↑F q.j = c₂ • 1
[PROOFSTEP]
rw [← F.map_mul, q.j_mul_j, F.map_smul, F.map_one]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.i * ↑F q.j = ↑F q.k
[PROOFSTEP]
rw [← F.map_mul, q.i_mul_j]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
F : A →ₐ[R] B
⊢ ↑F q.j * ↑F q.i = -↑F q.k
[PROOFSTEP]
rw [← F.map_mul, q.j_mul_i, F.map_neg]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ Basis.compHom (Basis.self R) (Basis.liftHom q) = q
[PROOFSTEP]
ext
[GOAL]
case hi
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ (Basis.compHom (Basis.self R) (Basis.liftHom q)).i = q.i
[PROOFSTEP]
simp [Basis.lift]
[GOAL]
case hj
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ (Basis.compHom (Basis.self R) (Basis.liftHom q)).j = q.j
[PROOFSTEP]
simp [Basis.lift]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
⊢ Basis.liftHom (Basis.compHom (Basis.self R) F) = F
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑(Basis.liftHom (Basis.compHom (Basis.self R) F)) x✝ = ↑F x✝
[PROOFSTEP]
dsimp [Basis.lift]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x✝.re + x✝.imI • ↑F { re := 0, imI := 1, imJ := 0, imK := 0 } +
        x✝.imJ • ↑F { re := 0, imI := 0, imJ := 1, imK := 0 } +
      x✝.imK • ↑F { re := 0, imI := 0, imJ := 0, imK := 1 } =
    ↑F x✝
[PROOFSTEP]
rw [← F.commutes]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑F (↑(algebraMap R ℍ[R,c₁,c₂]) x✝.re) + x✝.imI • ↑F { re := 0, imI := 1, imJ := 0, imK := 0 } +
        x✝.imJ • ↑F { re := 0, imI := 0, imJ := 1, imK := 0 } +
      x✝.imK • ↑F { re := 0, imI := 0, imJ := 0, imK := 1 } =
    ↑F x✝
[PROOFSTEP]
simp only [← F.commutes, ← F.map_smul, ← F.map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]
[GOAL]
case H
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ ↑F
      { re := x✝.re + 0 + 0 + 0, imI := 0 + x✝.imI • 1 + 0 + 0, imJ := 0 + 0 + x✝.imJ • 1 + 0,
        imK := 0 + 0 + 0 + x✝.imK • 1 } =
    ↑F x✝
[PROOFSTEP]
congr
[GOAL]
case H.h.e_6.h.e_re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ x✝.re + 0 + 0 + 0 = x✝.re
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + x✝.imI • 1 + 0 + 0 = x✝.imI
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + 0 + x✝.imJ • 1 + 0 = x✝.imJ
[PROOFSTEP]
simp
[GOAL]
case H.h.e_6.h.e_imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
F : ℍ[R,c₁,c₂] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂]
⊢ 0 + 0 + 0 + x✝.imK • 1 = x✝.imK
[PROOFSTEP]
simp
