awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
a : A
rw :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (fst (M := A) (inl a)) : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₁ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₂ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) 0 : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₃ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 * (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₄ :
  HAdd.hAdd (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 : B) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₅ rw₆ :
  Eq.{u_3 + 1} (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
⊢ Eq.{u_3 + 1} (α := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        (inl a) :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)

Tactic:
rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, map_zero, DualNumber.lift_apply_apply, TrivSqZeroExt.snd_inl, add_zero, TrivSqZeroExt.fst_inl
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
⊢ AlgHom.comp
      ((lift :
          (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
            A[ε] →ₐ[R] B)
        fe)
      (inlAlgHom R A A) =
    (↑fe : (A →ₐ[R] B) × B).1

Tactic:
AlgHom.ext <| lift_apply_inl fe

Premises used: AlgHom.ext, DualNumber.lift_apply_inl
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
⊢ (((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe :
          AlgHom.{u_1, u_4, u_3} R A[ε] B) :
        (a : A[ε]) → B)
      ε =
    (↑fe : (A →ₐ[R] B) × B).2

Tactic:
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, map_one, one_mul, zero_add]

Premises used: map_zero, zero_add, DualNumber.lift_apply_apply, map_one, DualNumber.fst_eps, DualNumber.snd_eps, one_mul
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := A[ε] →ₐ[R] TrivSqZeroExt A A)
    ((lift :
          (a :
              { fe : (A →ₐ[R] TrivSqZeroExt A A) × TrivSqZeroExt A A //
                fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → TrivSqZeroExt A A) a) }) →
            A[ε] →ₐ[R] TrivSqZeroExt A A)
        (Subtype.mk (p := fun (fe : (A →ₐ[R] TrivSqZeroExt A A) × TrivSqZeroExt A A) ↦
          fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → TrivSqZeroExt A A) a)) (inlAlgHom R A A, ε) ⋯) :
      A[ε] →ₐ[R] TrivSqZeroExt A A)
    (AlgHom.id R A[ε] : A[ε] →ₐ[R] A[ε])

Tactic:
lift.apply_symm_apply <| AlgHom.id R A[ε]

Premises used: Equiv.apply_symm_apply, TrivSqZeroExt.inr, DualNumber, AlgHom.id, TrivSqZeroExt.inl, TrivSqZeroExt.inlAlgHom, DualNumber.lift, AlgHom.comp, DualNumber.eps
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ⊤

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
refine :
  ∀ (x : TrivSqZeroExt A A) (hx : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) ⊤ x),
    Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) x
⊢ Eq (α := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
rw :
  Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) x

Tactic:
rw [← x.inl_fst_add_inr_snd_eq, inr_eq_smul_eps, ← inl_mul_eq_smul]

Premises used: TrivSqZeroExt.inl_fst_add_inr_snd_eq, TrivSqZeroExt.inl_mul_eq_smul, DualNumber.inr_eq_smul_eps
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)

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

Premises used: AddMemClass.add_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
refine_1 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)
refine_2 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.snd)
refine_3 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ε
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)

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

Premises used: AddMemClass.add_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)

Tactic:
le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.fst

Premises used: Set.mem_range_self, le_sup_left, TrivSqZeroExt.fst
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)

Tactic:
exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.fst

Premises used: Set.mem_range_self, le_sup_left, TrivSqZeroExt.fst
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.snd)

Tactic:
le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.snd

Premises used: Set.mem_range_self, TrivSqZeroExt.snd, le_sup_left
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.snd)

Tactic:
exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.snd

Premises used: Set.mem_range_self, TrivSqZeroExt.snd, le_sup_left
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ε

Tactic:
le_sup_right (α := Subalgebra R _) <| subset_adjoin <| Set.mem_singleton ε

Premises used: Set.mem_singleton, Algebra.subset_adjoin, le_sup_right, DualNumber.eps
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ε

Tactic:
refine le_sup_right (α := Subalgebra R _) <| subset_adjoin <| Set.mem_singleton ε

Premises used: Set.mem_singleton, Algebra.subset_adjoin, le_sup_right, DualNumber.eps
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst (M := ℍ[R])
      ({ re := TrivSqZeroExt.fst (x * y).re, imI := TrivSqZeroExt.fst (x * y).imI, imJ := TrivSqZeroExt.fst (x * y).imJ,
          imK := TrivSqZeroExt.fst (x * y).imK },
        { re := TrivSqZeroExt.snd (x * y).re, imI := TrivSqZeroExt.snd (x * y).imI,
          imJ := TrivSqZeroExt.snd (x * y).imJ, imK := TrivSqZeroExt.snd (x * y).imK }) =
    TrivSqZeroExt.fst
      (HMul.hMul (α := DualNumber ℍ[R])
        ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
        ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }))

Tactic:
rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h2 :
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re -
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI) -
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ) -
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI -
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ -
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI -
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ -
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK)
⊢ TrivSqZeroExt.snd (x * y).re =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).re +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).re

Tactic:
simp
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h2 :
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI +
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re) +
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK) -
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re +
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK -
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re +
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK -
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ)
⊢ TrivSqZeroExt.snd (x * y).imI =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imI +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imI

Tactic:
simp
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h2 :
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ -
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK) +
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re) +
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK +
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re +
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK +
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re +
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI)
⊢ TrivSqZeroExt.snd (x * y).imJ =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imJ +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h2 :
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK +
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ) -
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI) +
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ -
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI +
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ -
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI +
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re)
⊢ TrivSqZeroExt.snd (x * y).imK =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imK +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imK

Tactic:
simp
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re -
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI) -
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ) -
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI -
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ -
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI -
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ -
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK)

Tactic:
ring
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI +
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re) +
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK) -
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re +
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK -
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re +
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK -
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ)

Tactic:
ring
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ -
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK) +
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re) +
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK +
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re +
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK +
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re +
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI)

Tactic:
ring
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK +
          (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ) -
        (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI) +
      (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re) =
    TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ -
          TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI +
        TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re +
      (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ -
          TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI +
        TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re)

Tactic:
ring
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ ({ re := TrivSqZeroExt.fst (x + y).re, imI := TrivSqZeroExt.fst (x + y).imI, imJ := TrivSqZeroExt.fst (x + y).imJ,
        imK := TrivSqZeroExt.fst (x + y).imK },
      { re := TrivSqZeroExt.snd (x + y).re, imI := TrivSqZeroExt.snd (x + y).imI, imJ := TrivSqZeroExt.snd (x + y).imJ,
        imK := TrivSqZeroExt.snd (x + y).imK }) =
    HAdd.hAdd (α := DualNumber ℍ[R])
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
      ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] })

Tactic:
rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.re (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.fst (M := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.fst q.re

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.fst (M := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.fst q.imI

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.fst (M := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.fst q.imJ

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualQuaternion
Goal:
R : Type u_1
inst : CommRing R
q : ℍ[DualNumber R]
⊢ QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1)
      (TrivSqZeroExt.fst (M := ℍ[R]) ((dualNumberEquiv : (a : ℍ[DualNumber R]) → DualNumber ℍ[R]) q)) =
    TrivSqZeroExt.fst q.imK

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl