∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (x : Lean.Grind.CommRing.Mon)
  (h_1 : (x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x)
  (h_2 : (x : Lean.Grind.CommRing.Mon) → motive x Lean.Grind.CommRing.Mon.unit)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.unit, x with
    | Lean.Grind.CommRing.Mon.unit, x => h_1 x
    | x, Lean.Grind.CommRing.Mon.unit => h_2 x
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
    h_1 x