∀ {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} {x : Q(«$α»)} {e : Q(ℕ)} {b : Q(«$α»)}
  {a : Mathlib.Tactic.Ring.ExBase sα x} {a_1 : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ e}
  {a_2 : Mathlib.Tactic.Ring.ExProd sα b} {a_3 : Mathlib.Tactic.Ring.ExBase sα x}
  {a_4 : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ e} {a_5 : Mathlib.Tactic.Ring.ExProd sα b},
  Mathlib.Tactic.Ring.ExProd.mul a a_1 a_2 = Mathlib.Tactic.Ring.ExProd.mul a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5