∀ (_x : (_ : Lean.Grind.CommRing.Mon) ×' Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.sharesVar._unary _x =
    PSigma.casesOn _x fun a a_1 =>
      match a, a_1 with
      | Lean.Grind.CommRing.Mon.unit, x => false
      | x, Lean.Grind.CommRing.Mon.unit => false
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
        match compare pw₁.x pw₂.x with
        | Ordering.eq => true
        | Ordering.lt => Lean.Grind.CommRing.Mon.sharesVar._unary ⟨m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂⟩
        | Ordering.gt => Lean.Grind.CommRing.Mon.sharesVar._unary ⟨Lean.Grind.CommRing.Mon.mult pw₁ m₁, m₂⟩