Divide and conquer tactic for n-ary function

Stream: lean4

[Dean Young]

Suppose I have a function f : X → Y → Z``, or f : X × Y → Z, or maybe one which uses infix notation like ∘. I want to show that f x₁ y₁ = f x₂ y₂ by "divide_and_conquer" in tactic mode begin...end. i.e. I want new goals x₁ = x₂ and y₁ = y₂. What is the name for that tactic, and does it work for both f : X → Y → Z``and f : X × Y → Z? What about n-ary operations?

[Siddhartha Gadgil]

cogr tactic may do this.

[Reid Barton]

(congr)