-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompute.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  {toRingCompare : Mathlib.Tactic.Ring.Common.RingCompare BaseType}
  {add :
    {x y : Q(«$α»)} →
      BaseType x →
        BaseType y →
          Lean.MetaM
            (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» + «$y») ×
              Option Q(Mathlib.Meta.NormNum.IsNat («$x» + «$y») 0))}
  {mul :
    {x y : Q(«$α»)} → BaseType x → BaseType y → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» * «$y»))}
  {cast :
    (v : Lean.Level) →
      (β : Q(Type v)) →
        Q(CommSemiring «$β») →
          (x : Q(SMul «$β» «$α»)) →
            (x_1 : Q(«$β»)) →
              Mathlib.Tactic.AtomM
                ((y : Q(«$α»)) ×
                  Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$y») × Q(∀ (a : «$α»), «$x_1» • a = «$y» * a))}
  {neg :
    {x : Q(«$α»)} →
      (rα : Q(CommRing «$α»)) → BaseType x → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(-«$x»))}
  {pow :
    {x : Q(«$α»)} →
      {b : Q(ℕ)} →
        BaseType x →
          Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
            OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» ^ «$b»))}
  {inv :
    {x : Q(«$α»)} →
      Option Q(CharZero «$α») →
        (fα : Q(Semifield «$α»)) →
          BaseType x → Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x»⁻¹)))}
  {derive :
    (x : Q(«$α»)) →
      Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum BaseType sα) q(«$x»))}
  {isOne : {x : Q(«$α»)} → BaseType x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)}
  {one : Mathlib.Tactic.Ring.Common.Result BaseType q(Nat.rawCast 1)}
  {toRingCompare_1 : Mathlib.Tactic.Ring.Common.RingCompare BaseType}
  {add_1 :
    {x y : Q(«$α»)} →
      BaseType x →
        BaseType y →
          Lean.MetaM
            (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» + «$y») ×
              Option Q(Mathlib.Meta.NormNum.IsNat («$x» + «$y») 0))}
  {mul_1 :
    {x y : Q(«$α»)} → BaseType x → BaseType y → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» * «$y»))}
  {cast_1 :
    (v : Lean.Level) →
      (β : Q(Type v)) →
        Q(CommSemiring «$β») →
          (x : Q(SMul «$β» «$α»)) →
            (x_1 : Q(«$β»)) →
              Mathlib.Tactic.AtomM
                ((y : Q(«$α»)) ×
                  Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$y») × Q(∀ (a : «$α»), «$x_1» • a = «$y» * a))}
  {neg_1 :
    {x : Q(«$α»)} →
      (rα : Q(CommRing «$α»)) → BaseType x → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(-«$x»))}
  {pow_1 :
    {x : Q(«$α»)} →
      {b : Q(ℕ)} →
        BaseType x →
          Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
            OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» ^ «$b»))}
  {inv_1 :
    {x : Q(«$α»)} →
      Option Q(CharZero «$α») →
        (fα : Q(Semifield «$α»)) →
          BaseType x → Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x»⁻¹)))}
  {derive_1 :
    (x : Q(«$α»)) →
      Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum BaseType sα) q(«$x»))}
  {isOne_1 : {x : Q(«$α»)} → BaseType x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)}
  {one_1 : Mathlib.Tactic.Ring.Common.Result BaseType q(Nat.rawCast 1)},
  { toRingCompare := toRingCompare, add := add, mul := mul, cast := cast, neg := neg, pow := pow, inv := inv,
        derive := derive, isOne := isOne, one := one } =
      { toRingCompare := toRingCompare_1, add := add_1, mul := mul_1, cast := cast_1, neg := neg_1, pow := pow_1,
        inv := inv_1, derive := derive_1, isOne := isOne_1, one := one_1 } →
    toRingCompare = toRingCompare_1 ∧
      add = add_1 ∧
        mul = mul_1 ∧
          cast = cast_1 ∧ neg = neg_1 ∧ pow = pow_1 ∧ inv = inv_1 ∧ derive = derive_1 ∧ isOne = isOne_1 ∧ one = one_1