∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a₁ b₁ a₂ b₂ : α × α},
  Lean.Grind.Ring.OfSemiring.r α a₁ a₂ →
    Lean.Grind.Ring.OfSemiring.r α b₁ b₂ →
      (fun x x_1 =>
            match x with
            | (a, b) =>
              match x_1 with
              | (c, d) => Lean.Grind.Ring.OfSemiring.Q.mk (a + d, c + b))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | (a, b) =>
              match x_1 with
              | (c, d) => Lean.Grind.Ring.OfSemiring.Q.mk (a + d, c + b))
          a₂ b₂