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
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) (c₁ * c₃ * x.imK * y.imK) 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 +
        -((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_comm _ c₁]
-- 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 +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 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 * 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_right_comm _ _ c₃]
-- 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 * 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
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 * 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]
-- 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 * 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
have 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
Tactic: simp only [re_mul, sub_eq_add_neg, add_smul, neg_smul, imI_mul, ← add_assoc, imJ_mul, imK_mul]
-- 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
B : Basis A c₁ c₂ c₃
⊢ B.liftHom.range = R[B.i, B.j, B.k]
have a : B.liftHom.range ≤ R[B.i, B.j, B.k]
Tactic: apply le_antisymm
-- 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
B : Basis A c₁ c₂ c₃
a : B.liftHom.range ≤ R[B.i, B.j, B.k]
⊢ B.liftHom.range = R[B.i, B.j, B.k]
have a₁ : R[B.i, B.j, B.k] ≤ B.liftHom.range
Tactic: apply le_antisymm
-- 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
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)
have a : Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((algebraMap R A : (a : R) → A) y.re : A)
Tactic: refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
-- 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
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)
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) y : A)
have a₁ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imI • B.i)
Tactic: refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
-- 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
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)
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) y : A)
have a₂ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imJ • B.j)
Tactic: refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
-- 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
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)
⊢ Membership.mem (α := A) (γ := Subalgebra R A) R[B.i, B.j, B.k] ((B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) y : A)
have a₃ : Membership.mem (γ := Subalgebra R A) R[B.i, B.j, B.k] (y.imK • B.k)
Tactic: refine add_mem (add_mem (add_mem ?_ ?_) ?_) ?_
-- 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
B : Basis A c₁ c₂ c₃
⊢ R[B.i, B.j, B.k] ≤ B.liftHom.range
have a : {B.i, B.j, B.k} ⊆ (↑B.liftHom.range : Set A)
Tactic: rw [Algebra.adjoin_le_iff]
-- 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
B : Basis A c₁ c₂ c₃
⊢ B.i ∈ (↑B.liftHom.range : Set A)
have h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (i (Basis.self R)) = B.i
Tactic: use (Basis.self R).i
-- 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
B : Basis A c₁ c₂ c₃
⊢ B.j ∈ (↑B.liftHom.range : Set A)
have h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (j (Basis.self R)) = B.j
Tactic: use (Basis.self R).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
B : Basis A c₁ c₂ c₃
⊢ B.k ∈ (↑B.liftHom.range : Set A)
have h : (B.liftHom.toRingHom : (a : ℍ[R,c₁,c₂,c₃]) → A) (k (Basis.self R)) = B.k
Tactic: use (Basis.self R).k
-- 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
-- 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.j : B) = HSMul.hSMul (β := B) c₃ 1
have rw : (F : (a : A) → B) (q.j * q.j) = HSMul.hSMul (β := B) c₃ 1
Tactic: rw [← map_mul, q.j_mul_j, map_smul, map_one]
-- 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw : (F : (a : A) → B) (q.j * q.j) = 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
have rw₁ : (F : (a : A) → B) (HSMul.hSMul (β := A) c₃ 1) = HSMul.hSMul (β := B) c₃ 1
Tactic: rw [← map_mul, q.j_mul_j, map_smul, map_one]
-- 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
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
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.j : B) = HSMul.hSMul (β := B) c₃ 1
have rw₂ : HSMul.hSMul (β := B) c₃ ((F : (a : A) → B) 1 : B) = HSMul.hSMul (β := B) c₃ 1
Tactic: rw [← map_mul, q.j_mul_j, map_smul, map_one]
-- 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
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
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.j : B) = HSMul.hSMul (β := B) c₃ 1
have rw₃ : HSMul.hSMul (β := B) c₃ 1 = HSMul.hSMul (β := B) c₃ 1
Tactic: rw [← map_mul, q.j_mul_j, map_smul, map_one]
-- 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] 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
have rw : Eq.{u_3 + 1} (α := B) ((F : (a : A) → B) (q.i * q.j) : B) ((F : (a : A) → B) q.k : B)
Tactic: rw [← map_mul, q.i_mul_j]
-- 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
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)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.i : B) ((F : (a : A) → B) q.j : B) = (F : (a : A) → B) q.k
have rw₁ : Eq.{u_3 + 1} (α := B) ((F : (a : A) → B) q.k : B) ((F : (a : A) → B) q.k : B)
Tactic: rw [← map_mul, q.i_mul_j]
-- 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] 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)
have 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)
Tactic: rw [← map_mul, q.j_mul_i, map_sub, map_smul]