Can you elaborate on what the link to #11352 here is? Do you want that PR in before this one?

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

If you look at #11352, you will see that sum_lift₂ is a special case of sum_lex_lift, which is itself a special case of

def ultimate_sum_lift : Π (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂), finset (γ₁ ⊕ γ₂)
| (inl a) (inl b) := (f₁ a b).map ⟨_, inl_injective⟩
| (inl a) (inr b) := (g₁ a b).disj_sum (g₂ a b)
| (inr a) (inl b) := (h₁ a b).disj_sum (h₂ a b)
| (inr a) (inr b) := (f₂ a b).map ⟨_, inr_injective⟩

and I was wondering

• whether sum_lift₂ should live
• which generality you wanted me to use

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests