双射诱导的环结构：Isabelle/HOL简化证明方法问询

给定一个环，以及到另一集合（注：为集合而非类型）的双射，理应可在该集合上定义唯一的诱导环结构，使该双射成为同构。但当前实现该思路的证明（含定义与引理）长达101行，现询问是否可通过“提升”等方法实现更简洁自然的证明。

待补充的Isabelle/HOL示例代码如下：

theory InducedRing
  imports "HOL-Algebra.QuotRing"
begin

lemma
  assumes "ring ℛ" "bij_betw φ (carrier ℛ) S"
  obtains 𝒮 where "ring 𝒮" and "carrier 𝒮 = S" and "φ ∈ ring_hom ℛ 𝒮"
  sorry

end

可改写为等价或更强的命题（如反转φ方向、假设互逆双射、将假设纳入locale定义、断言𝒮的唯一性等），目标是使证明简洁自然，希望借助HOL-Algebra或其他库中的定理实现，但sledgehammer未找到适配当前命题的定理。

内容的提问来源于stack exchange，提问作者Charles Staats