∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₁)
  (b : β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inr b) = (g₁ a b).disjSum (g₂ a b)