feat(data/sym/sym2): sym2.lift₂ (#15887)

We add `sym2.lift₂`, a two-argument version of `sym2.lift`. Its intended purpose is for defining the relation on unordered pairs relating pairs where exactly one entry decreases.

We also generalize the types for the existing `funext₂` and `funext₃`.

src/data/sym/sym2.lean

@@ -94,9 +94,14 @@ protected lemma ind {f : sym2 α → Prop} (h : ∀ x y, f ⟦(x, y)⟧) : ∀ i
 quotient.ind $ prod.rec $ by exact h
 
 @[elab_as_eliminator]
-protected lemma induction_on {f : sym2 α → Prop} (i : sym2 α) (hf : ∀ x y, f ⟦(x,y)⟧) : f i :=
+protected lemma induction_on {f : sym2 α → Prop} (i : sym2 α) (hf : ∀ x y, f ⟦(x, y)⟧) : f i :=
 i.ind hf
 
+@[elab_as_eliminator]
+protected lemma induction_on₂ {f : sym2 α → sym2 β → Prop} (i : sym2 α) (j : sym2 β)
+  (hf : ∀ a₁ a₂ b₁ b₂, f ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧) : f i j :=
+quotient.induction_on₂ i j $ by { rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩, exact hf _ _ _ _ }
+
 protected lemma «exists» {α : Sort*} {f : sym2 α → Prop} :
   (∃ (x : sym2 α), f x) ↔ ∃ x y, f ⟦(x, y)⟧ :=
 (surjective_quotient_mk _).exists.trans prod.exists
@@ -142,6 +147,27 @@ lemma lift_mk (f : {f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂
 lemma coe_lift_symm_apply (F : sym2 α → β) (a₁ a₂ : α) :
   (lift.symm F : α → α → β) a₁ a₂ = F ⟦(a₁, a₂)⟧ := rfl
 
+/-- A two-argument version of `sym2.lift`. -/
+def lift₂ : {f : α → α → β → β → γ // ∀ a₁ a₂ b₁ b₂,
+  f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁} ≃ (sym2 α → sym2 β → γ) :=
+{ to_fun := λ f, quotient.lift₂ (λ (a : α × α) (b : β × β), f.1 a.1 a.2 b.1 b.2) begin
+    rintro _ _ _ _ ⟨⟩ ⟨⟩,
+    exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]
+  end,
+  inv_fun := λ F, ⟨λ a₁ a₂ b₁ b₂, F ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧, λ a₁ a₂ b₁ b₂,
+    by { split, exacts [congr_arg2 F eq_swap rfl, congr_arg2 F rfl eq_swap] }⟩,
+  left_inv := λ f, subtype.ext rfl,
+  right_inv := λ F, funext₂ $ λ a b, sym2.induction_on₂ a b $ λ _ _ _ _, rfl }
+
+@[simp]
+lemma lift₂_mk (f : {f : α → α → β → β → γ // ∀ a₁ a₂ b₁ b₂,
+  f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁}) (a₁ a₂ : α) (b₁ b₂ : β) :
+  lift₂ f ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧ = (f : α → α → β → β → γ) a₁ a₂ b₁ b₂ := rfl
+
+@[simp]
+lemma coe_lift₂_symm_apply (F : sym2 α → sym2 β → γ) (a₁ a₂ : α) (b₁ b₂ : β) :
+  (lift₂.symm F : α → α → β → β → γ) a₁ a₂ b₁ b₂ = F ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧ := rfl
+
 /--
 The functor `sym2` is functorial, and this function constructs the induced maps.
 -/

src/logic/basic.lean

@@ -914,10 +914,10 @@ lemma congr_fun₃ {f g : Π a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c
   f a b c = g a b c :=
 congr_fun₂ (congr_fun h _) _ _
 
-lemma funext₂ {f g : Π a, β a → Prop} (h : ∀ a b, f a b = g a b) : f = g :=
+lemma funext₂ {f g : Π a b, γ a b} (h : ∀ a b, f a b = g a b) : f = g :=
 funext $ λ _, funext $ h _
 
-lemma funext₃ {f g : Π a b, γ a b → Prop} (h : ∀ a b c, f a b c = g a b c) : f = g :=
+lemma funext₃ {f g : Π a b c, δ a b c} (h : ∀ a b c, f a b c = g a b c) : f = g :=
 funext $ λ _, funext₂ $ h _
 
 end equality