awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuaternionBasis
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₃]
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 * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
⊢ 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 +
          -((c₁ * (x.imK * y.imI)) • 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₃]

Premises used: mul_right_comm
-- Module: Mathlib.Algebra.QuaternionBasis
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₃]
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 * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
⊢ 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 * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.QuaternionBasis
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₃]
simp :
  HSMul.hSMul (β := A) (x.re * y.re) 1 + HSMul.hSMul (β := A) (c₁ * x.imI * y.imI) 1 +
                                        HSMul.hSMul (β := A) (c₃ * x.imJ * y.imJ) 1 +
                                      HSMul.hSMul (β := A) (c₂ * c₃ * x.imJ * y.imK) 1 +
                                    -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
                                  (x.re * y.imI) • q.i +
                                (x.imI * y.re) • q.i +
                              (c₂ * x.imI * y.imI) • 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.imJ * y.imI) • q.j +
                -((c₁ * x.imK * y.imI) • q.j) +
              (x.re * y.imK) • q.k +
            (x.imI * y.imJ) • q.k +
          (c₂ * x.imI * y.imK) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • 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 * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
⊢ 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 * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1

Tactic:
simp only [re_mul, sub_eq_add_neg, add_smul, neg_smul, imI_mul, ← add_assoc, imJ_mul, imK_mul]

Premises used: neg_smul, add_assoc, sub_eq_add_neg, QuaternionAlgebra.re_mul, QuaternionAlgebra.imK_mul, add_smul, QuaternionAlgebra.imJ_mul, QuaternionAlgebra.imI_mul
-- Module: Mathlib.Algebra.QuaternionBasis
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.re * y.re) 1 + HSMul.hSMul (β := A) (c₁ * x.imI * y.imI) 1 +
                                            HSMul.hSMul (β := A) (c₃ * x.imJ * y.imJ) 1 +
                                          HSMul.hSMul (β := A) (c₂ * c₃ * x.imJ * y.imK) 1 +
                                        -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
                                      (x.re * y.imI) • q.i +
                                    (x.imI * y.re) • q.i +
                                  (c₂ * x.imI * y.imI) • 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.imJ * y.imI) • q.j +
                    -((c₁ * x.imK * y.imI) • q.j) +
                  (x.re * y.imK) • q.k +
                (x.imI * y.imJ) • q.k +
              (c₂ * x.imI * y.imK) • q.k +
            -((x.imJ * y.imI) • q.k) +
          (x.imK * y.re) • q.k +
        0 -
      (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 * c₃ * y.imJ) 1 +
                  (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
                (x.imK * y.re) • q.k +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.imK * c₃ * y.imJ) • q.i +
          -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
        0) =
    0

Tactic:
module
-- Module: Mathlib.Algebra.QuaternionBasis
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₃
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (r • x) = r • q.lift x

Tactic:
simp [lift, mul_smul, ← Algebra.smul_def]

Premises used: QuaternionAlgebra.Basis.lift, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
a : B.liftHom.range ≤ R[B.i, B.j, B.k]
a₁ : R[B.i, B.j, B.k] ≤ B.liftHom.range
⊢ B.liftHom.range = R[B.i, B.j, B.k]

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) y : A)

Tactic:
add_mem (add_mem (add_mem ?_ ?_) ?_) ?_

Premises used: Set.Mem, QuaternionAlgebra.Basis.lift, AddMemClass.add_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
a : Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((algebraMap R A : (a : R) → A) y.re : A)
a₁ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imI • B.i)
a₂ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imJ • B.j)
a₃ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imK • B.k)
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) y : A)

Tactic:
refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((algebraMap R A : (a : R) → A) y.re : A)

Tactic:
algebraMap_mem _ _

Premises used: algebraMap_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((algebraMap R A : (a : R) → A) y.re : A)

Tactic:
exact algebraMap_mem _ _

Premises used: algebraMap_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Set A) {B.i, B.j, B.k} B.i

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imI • B.i)

Tactic:
exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

Premises used: Algebra.subset_adjoin, Subalgebra.smul_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Set A) {B.i, B.j, B.k} B.j

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imJ • B.j)

Tactic:
exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

Premises used: Algebra.subset_adjoin, Subalgebra.smul_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Set A) {B.i, B.j, B.k} B.k

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imK • B.k)

Tactic:
exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

Premises used: Algebra.subset_adjoin, Subalgebra.smul_mem
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
a : {B.i, B.j, B.k} ⊆ (↑B.liftHom.range : Set A)
⊢ R[B.i, B.j, B.k] ≤ B.liftHom.range

Tactic:
rw [Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (i (Basis.self R)) = B.i
⊢ B.i ∈ (↑B.liftHom.range : Set A)

Tactic:
use (Basis.self R).i

Premises used: QuaternionAlgebra.Basis.self, QuaternionAlgebra.Basis.i
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (j (Basis.self R)) = B.j
⊢ B.j ∈ (↑B.liftHom.range : Set A)

Tactic:
use (Basis.self R).j

Premises used: QuaternionAlgebra.Basis.self, QuaternionAlgebra.Basis.j
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (k (Basis.self R)) = B.k
⊢ B.k ∈ (↑B.liftHom.range : Set A)

Tactic:
use (Basis.self R).k

Premises used: QuaternionAlgebra.Basis.self, QuaternionAlgebra.Basis.k
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
⊢ (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (i (Basis.self R)) = B.i

Tactic:
simp [lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
⊢ (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (j (Basis.self R)) = B.j

Tactic:
simp [lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
B : Basis A c₁ c₂ c₃
⊢ (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (k (Basis.self R)) = B.k

Tactic:
simp [lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw : (F : (a : A) → B) (q.i * q.i) = HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
rw₁ :
  (F : (a : A) → B) (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((F : (a : A) → B) (HSMul.hSMul (β := A) c₁ 1) : B) ((F : (a : A) → B) (c₂ • q.i) : B) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
rw₃ :
  HAdd.hAdd (β := B) (HSMul.hSMul (β := B) c₁ ((F : (a : A) → B) 1 : B)) ((F : (a : A) → B) (c₂ • q.i) : B) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
rw₄ :
  HSMul.hSMul (β := B) c₁ ((F : (a : A) → B) 1 : B) + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
rw₅ rw₆ :
  HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.i : B) ((F : (a : A) → B) q.i : B) =
    HSMul.hSMul (β := B) c₁ 1 + HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.i : B)

Tactic:
rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]

Premises used: QuaternionAlgebra.Basis.i_mul_i, map_add, map_mul, map_one, map_smul
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw : (F : (a : A) → B) (q.j * q.j) = HSMul.hSMul (β := B) c₃ 1
rw₁ : (F : (a : A) → B) (HSMul.hSMul (β := A) c₃ 1) = HSMul.hSMul (β := B) c₃ 1
rw₂ : HSMul.hSMul (β := B) c₃ ((F : (a : A) → B) 1 : B) = HSMul.hSMul (β := B) c₃ 1
rw₃ rw₄ : HSMul.hSMul (β := B) c₃ 1 = HSMul.hSMul (β := B) c₃ 1
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.j : B) = HSMul.hSMul (β := B) c₃ 1

Tactic:
rw [← map_mul, q.j_mul_j, map_smul, map_one]

Premises used: QuaternionAlgebra.Basis.j_mul_j, map_mul, map_one, map_smul
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw : Eq.{u_3 + 1} (α := B) ((F : (a : A) → B) (q.i * q.j) : B) ((F : (a : A) → B) q.k : B)
rw₁ rw₂ : Eq.{u_3 + 1} (α := B) ((F : (a : A) → B) q.k : B) ((F : (a : A) → B) q.k : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.i : B) ((F : (a : A) → B) q.j : B) = (F : (a : A) → B) q.k

Tactic:
rw [← map_mul, q.i_mul_j]

Premises used: QuaternionAlgebra.Basis.i_mul_j, map_mul
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw :
  (F : (a : A) → B) (q.j * q.i) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₁ :
  (F : (a : A) → B) (c₂ • q.j - q.k) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₂ :
  HSub.hSub (α := B) (β := B) ((F : (a : A) → B) (c₂ • q.j) : B) ((F : (a : A) → B) q.k : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₃ rw₄ :
  HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.i : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)

Tactic:
rw [← map_mul, q.j_mul_i, map_sub, map_smul]

Premises used: map_sub, map_mul, QuaternionAlgebra.Basis.j_mul_i, map_smul
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
hi : (Basis.compHom (Basis.self R) q.liftHom).i = q.i
hj : (Basis.compHom (Basis.self R) q.liftHom).j = q.j
⊢ Basis.compHom (Basis.self R) q.liftHom = q

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
⊢ (Basis.compHom (Basis.self R) q.liftHom).i = q.i

Tactic:
simp [Basis.lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
q : Basis A c₁ c₂ c₃
⊢ (Basis.compHom (Basis.self R) q.liftHom).j = q.j

Tactic:
simp [Basis.lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
H :
  ∀ (x : ℍ[R,c₁,c₂,c₃]),
    Eq.{u_2 + 1} (α := A) (((Basis.compHom (Basis.self R) F).liftHom : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
      ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
⊢ (Basis.compHom (Basis.self R) F).liftHom = F

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
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
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
H :
  HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A)
          (HSMul.hSMul (β := A) x.imI
            ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
        HSMul.hSMul (β := A) x.imJ
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
      HSMul.hSMul (β := A) x.imK
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
    (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
⊢ Eq.{u_2 + 1} (α := A) (((Basis.compHom (Basis.self R) F).liftHom : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)

Tactic:
dsimp [Basis.lift]

Premises used: QuaternionAlgebra.Basis.lift
-- Module: Mathlib.Algebra.QuaternionBasis
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
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
H :
  HAdd.hAdd (α := A)
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) x.re : ℍ[R,c₁,c₂,c₃]) :
            A)
          (HSMul.hSMul (β := A) x.imI
            ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
        HSMul.hSMul (β := A) x.imJ
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
      HSMul.hSMul (β := A) x.imK
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
    (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
⊢ HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A)
          (HSMul.hSMul (β := A) x.imI
            ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
        HSMul.hSMul (β := A) x.imJ
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
      HSMul.hSMul (β := A) x.imK
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
    (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x

Tactic:
rw [← F.commutes]

Premises used: AlgHom.commutes