-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompute.mk.injEq : ∀ {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)