awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }
have imK : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
  imK (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 }
have re : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
  (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 }
have imI : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
  (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imI
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 }
have imJ : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
  (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imI
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imJ
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 }
have imK : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
  (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₃ : HSMul.hSMul (β := A) c₁ 1 * q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₃ : HSMul.hSMul (β := A) c₁ 1 * q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₄ : c₁ • (1 * q.j) + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₃ : HSMul.hSMul (β := A) c₁ 1 * q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₄ : c₁ • (1 * q.j) + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₅ : c₁ • q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₃ : HSMul.hSMul (β := A) c₁ 1 * q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₄ : c₁ • (1 * q.j) + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₅ : c₁ • q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k
have rw₆ : c₁ • q.j + c₂ • (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
Tactic: rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.i = -c₁ • q.j
have rw : c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)
Tactic: rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)
have a : c₂ • q.k - (c₁ • q.j + c₂ • q.k) + 0 - (-(c₁ • q.j) + 0) = 0
Tactic: linear_combination (norm := module)
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.j = c₃ • q.i
have rw : q.i * q.j * q.j = c₃ • q.i
Tactic: rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * q.j * q.j = c₃ • q.i
⊢ q.k * q.j = c₃ • q.i
have rw₁ : q.i * (q.j * q.j) = c₃ • q.i
Tactic: rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * q.j * q.j = c₃ • q.i
rw₁ : q.i * (q.j * q.j) = c₃ • q.i
⊢ q.k * q.j = c₃ • q.i
have rw₂ : q.i * HSMul.hSMul (β := A) c₃ 1 = c₃ • q.i
Tactic: rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * q.j * q.j = c₃ • q.i
rw₁ : q.i * (q.j * q.j) = c₃ • q.i
rw₂ : q.i * HSMul.hSMul (β := A) c₃ 1 = c₃ • q.i
⊢ q.k * q.j = c₃ • q.i
have rw₃ : c₃ • (q.i * 1) = c₃ • q.i
Tactic: rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
rw : q.i * q.j * q.j = c₃ • q.i
rw₁ : q.i * (q.j * q.j) = c₃ • q.i
rw₂ : q.i * HSMul.hSMul (β := A) c₃ 1 = c₃ • q.i
rw₃ : c₃ • (q.i * 1) = c₃ • q.i
⊢ q.k * q.j = c₃ • q.i
have rw₄ : c₃ • q.i = c₃ • q.i
Tactic: rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.j * q.k = HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i
have rw : HSMul.hSMul (β := A) (c₂ • c₃) 1 - c₃ • q.i = HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i
Tactic: rw [← i_mul_j, ← mul_assoc, j_mul_i, sub_mul, smul_mul_assoc, j_mul_j, ← smul_assoc, k_mul_j]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.k = -HSMul.hSMul (β := A) (c₁ * c₃) 1
have rw : c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) =
  -HSMul.hSMul (β := A) (c₁ * c₃) 1
Tactic: rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ←
    mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm,
    smul_mul_assoc, mul_assoc, j_mul_j, add_mul, smul_mul_assoc, j_mul_j, smul_smul,
    smul_mul_assoc, mul_assoc, j_mul_j]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) =
    -HSMul.hSMul (β := A) (c₁ * c₃) 1
have a : c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) +
      0 -
    (-HSMul.hSMul (β := A) (c₁ * c₃) 1 + 0) =
  0
Tactic: linear_combination (norm := module)
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x + y) = q.lift x + q.lift y
have simp : HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) x.re : A) ((algebraMap R A : (a : R) → A) y.re : A) +
        (x.imI • q.i + y.imI • q.i) +
      (x.imJ • q.j + y.imJ • q.j) +
    (x.imK • q.k + y.imK • q.k) =
  HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A) (x.imI • q.i) + x.imJ • q.j + x.imK • q.k +
    (HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) y.re : A) (y.imI • q.i) + y.imJ • q.j + y.imK • q.k)
Tactic: simp only [lift, re_add, map_add, imI_add, add_smul, imJ_add, imK_add]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x * y) = q.lift x * q.lift y
have simp : HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
  (HSMul.hSMul (β := A) x.re 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) *
    (HSMul.hSMul (β := A) y.re 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
Tactic: simp only [lift, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (HSMul.hSMul (β := A) x.re 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) *
      (HSMul.hSMul (β := A) y.re 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
have simp_rw : HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
  HSMul.hSMul (β := A) (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))
Tactic: simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    HSMul.hSMul (β := A) (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))
have simp : HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
  HSMul.hSMul (β := A) (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) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) + (x.imI * y.imJ) • q.k +
          (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k)) +
      ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (c₂ • q.j - q.k) + (x.imJ * y.imJ) • HSMul.hSMul (β := A) c₃ 1 +
        (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 - 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) • -HSMul.hSMul (β := A) (c₁ * c₃) 1)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    HSMul.hSMul (β := A) (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) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) + (x.imI * y.imJ) • q.k +
            (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (c₂ • q.j - q.k) + (x.imJ * y.imJ) • HSMul.hSMul (β := A) c₃ 1 +
          (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 - 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) • -HSMul.hSMul (β := A) (c₁ * c₃) 1)
have simp : HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
  HSMul.hSMul (β := A) (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) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) +
                      (x.imI * y.imJ) • q.k +
                    (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                  (x.imJ * y.re) • q.j +
                (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
              HSMul.hSMul (β := A) (x.imJ * y.imJ * c₃) 1 +
            (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
          (x.imK * y.re) • q.k +
        -((x.imK * y.imI * c₁) • q.j) +
      (x.imK * y.imJ * c₃) • q.i +
    -HSMul.hSMul (β := A) (x.imK * y.imK * (c₁ * c₃)) 1
Tactic: simp only [smul_smul, smul_neg, sub_eq_add_neg, ← add_assoc, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    HSMul.hSMul (β := A) (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) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                HSMul.hSMul (β := A) (x.imJ * y.imJ * c₃) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (x.imK * y.imK * (c₁ * c₃)) 1
have simp : HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
  HSMul.hSMul (β := A) (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) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) +
                      (x.imI * y.imJ) • q.k +
                    (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                  (x.imJ * y.re) • q.j +
                (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
              HSMul.hSMul (β := A) (x.imJ * y.imJ * c₃) 1 +
            (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
          (x.imK * y.re) • q.k +
        -((x.imK * y.imI * c₁) • q.j) +
      (x.imK * y.imJ * c₃) • q.i +
    -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
Tactic: simp only [mul_right_comm _ _ (c₁ * c₃), mul_comm _ (c₁ * c₃)]