∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (α : Sort u✝) (β : α → Sort v✝)
  (f : (x : α) → β x) (rel : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → α → Prop)
  (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 :
    Unit →
      ((y : α) → rel Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit y → β y) →
        motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) →
        ((y : α) → rel Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m) y → β y) →
          motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) →
        ((y : α) → rel (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit y → β y) →
          motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            ((y : α) → rel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂) y → β y) →
              motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  ((match (motive := (m₁ m₂ : Lean.Grind.CommRing.Mon) → ((y : α) → rel m₁ m₂ y → β y) → motive m₁ m₂) m₁, m₂ with
      | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => fun x => h_1 a x
      | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => fun x => h_2 p m x
      | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => fun x => h_3 p m x
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => fun x => h_4 pw₁ m₁ pw₂ m₂ x)
      fun y h => f y) =
    match m₁, m₂ with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 a fun y h => f y
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m fun y h => f y
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m fun y h => f y
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂ fun y h => f y