{R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                {motive : (A ≃ₐ[R] B) → Sort u_1} →
                  (t : A ≃ₐ[R] B) →
                    ((toEquiv : A ≃ B) →
                        (map_mul' : ∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y) →
                          (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) →
                            (commutes' : ∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r) →
                              motive
                                { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add',
                                  commutes' := commutes' }) →
                      motive t