feat(data/set/sups): Set family operations (#18172)

Followup to #17947. Add a similar `set` API (but do not define `set.disj_sups` because I don't need it), correct a few lemma names and connect to upper/lower sets.

Author: YaelDillies

src/data/finset/n_ary.lean

@@ -27,7 +27,7 @@ open function set
 
 namespace finset
 
-variables {α α' β β' γ γ' δ δ' ε ε' : Type*}
+variables {α α' β β' γ γ' δ δ' ε ε' ζ ζ' ν : Type*}
   [decidable_eq α'] [decidable_eq β'] [decidable_eq γ] [decidable_eq γ'] [decidable_eq δ]
   [decidable_eq δ'] [decidable_eq ε] [decidable_eq ε']
   {f f' : α → β → γ} {g g' : α → β → γ → δ} {s s' : finset α} {t t' : finset β} {u u' : finset γ}
@@ -71,11 +71,11 @@ lemma image₂_subset_left (ht : t ⊆ t') : image₂ f s t ⊆ image₂ f s t'
 lemma image₂_subset_right (hs : s ⊆ s') : image₂ f s t ⊆ image₂ f s' t :=
 image₂_subset hs subset.rfl
 
-lemma image_subset_image₂_left (hb : b ∈ t) : (λ a, f a b) '' s ⊆ image₂ f s t :=
-ball_image_of_ball $ λ a ha, mem_image₂_of_mem ha hb
+lemma image_subset_image₂_left (hb : b ∈ t) : s.image (λ a, f a b) ⊆ image₂ f s t :=
+image_subset_iff.2 $ λ a ha, mem_image₂_of_mem ha hb
 
-lemma image_subset_image₂_right (ha : a ∈ s) : f a '' t ⊆ image₂ f s t :=
-ball_image_of_ball $ λ b, mem_image₂_of_mem ha
+lemma image_subset_image₂_right (ha : a ∈ s) : t.image (f a) ⊆ image₂ f s t :=
+image_subset_iff.2 $ λ b, mem_image₂_of_mem ha
 
 lemma forall_image₂_iff {p : γ → Prop} : (∀ z ∈ image₂ f s t, p z) ↔ ∀ (x ∈ s) (y ∈ t), p (f x y) :=
 by simp_rw [←mem_coe, coe_image₂, forall_image2_iff]
@@ -252,6 +252,13 @@ lemma image₂_right_comm {γ : Type*} {u : finset γ} {f : δ → γ → ε} {g
   image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t :=
 coe_injective $ by { push_cast, exact image2_right_comm h_right_comm }
 
+lemma image₂_image₂_image₂_comm {γ δ : Type*} {u : finset γ} {v : finset δ} [decidable_eq ζ]
+  [decidable_eq ζ'] [decidable_eq ν] {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ}
+  {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'}
+  (h_comm : ∀ a b c d, f (g a b) (h c d) = f' (g' a c) (h' b d)) :
+  image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) :=
+coe_injective $ by { push_cast, exact image2_image2_image2_comm h_comm }
+
 lemma image_image₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
   (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
   (image₂ f s t).image g = image₂ f' (s.image g₁) (t.image g₂) :=

src/data/finset/sups.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import data.finset.n_ary
+import data.set.sups
 
 /-!
 # Set family operations
@@ -12,16 +13,16 @@ This file defines a few binary operations on `finset α` for use in set family c
 
 ## Main declarations
 
-* `finset.sups s t`: Finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`.
-* `finset.infs s t`: Finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`.
+* `s ⊻ t`: Finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`.
+* `s ⊼ t`: Finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`.
 * `finset.disj_sups s t`: Finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t` and `a`
   and `b` are disjoint.
 
 ## Notation
 
 We define the following notation in locale `finset_family`:
-* `s ⊻ t` for `finset.sups s t`
-* `s ⊼ t` for `finset.infs s t`
+* `s ⊻ t`
+* `s ⊼ t`
 * `s ○ t` for `finset.disj_sups s t`
 
 ## References
@@ -30,25 +31,26 @@ We define the following notation in locale `finset_family`:
 -/
 
 open function
+open_locale set_family
 
 variables {α : Type*} [decidable_eq α]
 
 namespace finset
 section sups
-variables [semilattice_sup α] (s s₁ s₂ t t₁ t₂ u : finset α)
+variables [semilattice_sup α] (s s₁ s₂ t t₁ t₂ u v : finset α)
 
-/-- The finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`. -/
-def sups (s t : finset α) : finset α := image₂ (⊔) s t
+/-- `s ⊻ t` is the finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`. -/
+protected def has_sups : has_sups (finset α) := ⟨image₂ (⊔)⟩
 
-localized "infix (name := finset.sups) ` ⊻ `:74 := finset.sups" in finset_family
+localized "attribute [instance] finset.has_sups" in finset_family
 
 variables {s t} {a b c : α}
 
-@[simp] lemma mem_sups : c ∈ s ⊻ t ↔ ∃ (a ∈ s) (b ∈ t), a ⊔ b = c := by simp [sups]
+@[simp] lemma mem_sups : c ∈ s ⊻ t ↔ ∃ (a ∈ s) (b ∈ t), a ⊔ b = c := by simp [(⊻)]
 
 variables (s t)
 
-@[simp, norm_cast] lemma coe_sups : (s ⊻ t : set α) = set.image2 (⊔) s t := coe_image₂ _ _ _
+@[simp, norm_cast] lemma coe_sups : (↑(s ⊻ t) : set α) = s ⊻ t := coe_image₂ _ _ _
 
 lemma card_sups_le : (s ⊻ t).card ≤ s.card * t.card := card_image₂_le _ _ _
 
@@ -63,29 +65,28 @@ lemma sups_subset : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ 
 lemma sups_subset_left : t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂ := image₂_subset_left
 lemma sups_subset_right : s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t := image₂_subset_right
 
-lemma image_subset_sups_left : b ∈ t → (λ a, a ⊔ b) '' s ⊆ s ⊻ t := image_subset_image₂_left
-lemma image_subset_sups_right : a ∈ s → (⊔) a '' t ⊆ s ⊻ t := image_subset_image₂_right
+lemma image_subset_sups_left : b ∈ t → s.image (λ a, a ⊔ b) ⊆ s ⊻ t := image_subset_image₂_left
+lemma image_subset_sups_right : a ∈ s → t.image ((⊔) a) ⊆ s ⊻ t := image_subset_image₂_right
 
 lemma forall_sups_iff {p : α → Prop} : (∀ c ∈ s ⊻ t, p c) ↔ ∀ (a ∈ s) (b ∈ t), p (a ⊔ b) :=
 forall_image₂_iff
 
 @[simp] lemma sups_subset_iff : s ⊻ t ⊆ u ↔ ∀ (a ∈ s) (b ∈ t), a ⊔ b ∈ u := image₂_subset_iff
 
-@[simp] lemma sups_nonempty_iff : (s ⊻ t).nonempty ↔ s.nonempty ∧ t.nonempty := image₂_nonempty_iff
+@[simp] lemma sups_nonempty : (s ⊻ t).nonempty ↔ s.nonempty ∧ t.nonempty := image₂_nonempty_iff
 
-lemma nonempty.sups : s.nonempty → t.nonempty → (s ⊻ t).nonempty := nonempty.image₂
+protected lemma nonempty.sups : s.nonempty → t.nonempty → (s ⊻ t).nonempty := nonempty.image₂
 lemma nonempty.of_sups_left : (s ⊻ t).nonempty → s.nonempty := nonempty.of_image₂_left
 lemma nonempty.of_sups_right : (s ⊻ t).nonempty → t.nonempty := nonempty.of_image₂_right
 
-@[simp] lemma sups_empty_left : ∅ ⊻ t = ∅ := image₂_empty_left
-@[simp] lemma sups_empty_right : s ⊻ ∅ = ∅ := image₂_empty_right
-@[simp] lemma sups_eq_empty_iff : s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅ := image₂_eq_empty_iff
+@[simp] lemma empty_sups : ∅ ⊻ t = ∅ := image₂_empty_left
+@[simp] lemma sups_empty : s ⊻ ∅ = ∅ := image₂_empty_right
+@[simp] lemma sups_eq_empty : s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅ := image₂_eq_empty_iff
 
-@[simp] lemma sups_singleton_left : {a} ⊻ t = t.image (λ b, a ⊔ b) := image₂_singleton_left
-@[simp] lemma sups_singleton_right : s ⊻ {b} = s.image (λ a, a ⊔ b) := image₂_singleton_right
-lemma sups_singleton_left' : {a} ⊻ t = t.image ((⊔) a) := image₂_singleton_left'
+@[simp] lemma singleton_sups : {a} ⊻ t = t.image (λ b, a ⊔ b) := image₂_singleton_left
+@[simp] lemma sups_singleton : s ⊻ {b} = s.image (λ a, a ⊔ b) := image₂_singleton_right
 
-lemma sups_singleton : ({a} ⊻ {b} : finset α) = {a ⊔ b} := image₂_singleton
+lemma singleton_sups_singleton : ({a} ⊻ {b} : finset α) = {a ⊔ b} := image₂_singleton
 
 lemma sups_union_left : (s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t := image₂_union_left
 lemma sups_union_right : s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂ := image₂_union_right
@@ -94,10 +95,10 @@ lemma sups_inter_subset_left : (s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻
 lemma sups_inter_subset_right : s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂ := image₂_inter_subset_right
 
 lemma subset_sups {s t : set α} :
-  ↑u ⊆ set.image2 (⊔) s t → ∃ s' t' : finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t' :=
+  ↑u ⊆ s ⊻ t → ∃ s' t' : finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t' :=
 subset_image₂
 
-variables (s t u)
+variables (s t u v)
 
 lemma bUnion_image_sup_left : s.bUnion (λ a, t.image $ (⊔) a) = s ⊻ t := bUnion_image_left
 lemma bUnion_image_sup_right : t.bUnion (λ b, s.image $ λ a, a ⊔ b) = s ⊻ t := bUnion_image_right
@@ -109,24 +110,26 @@ lemma sups_assoc : (s ⊻ t) ⊻ u = s ⊻ (t ⊻ u) := image₂_assoc $ λ _ _
 lemma sups_comm : s ⊻ t = t ⊻ s := image₂_comm $ λ _ _, sup_comm
 lemma sups_left_comm : s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u) := image₂_left_comm sup_left_comm
 lemma sups_right_comm : (s ⊻ t) ⊻ u = (s ⊻ u) ⊻ t := image₂_right_comm sup_right_comm
+lemma sups_sups_sups_comm : (s ⊻ t) ⊻ (u ⊻ v) = (s ⊻ u) ⊻ (t ⊻ v) :=
+image₂_image₂_image₂_comm sup_sup_sup_comm
 
 end sups
 
 section infs
-variables [semilattice_inf α] (s s₁ s₂ t t₁ t₂ u : finset α)
+variables [semilattice_inf α] (s s₁ s₂ t t₁ t₂ u v : finset α)
 
-/-- The finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`. -/
-def infs (s t : finset α) : finset α := image₂ (⊓) s t
+/-- `s ⊼ t` is the finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`. -/
+protected def has_infs : has_infs (finset α) := ⟨image₂ (⊓)⟩
 
-localized "infix (name := finset.infs) ` ⊼ `:74 := finset.infs" in finset_family
+localized "attribute [instance] finset.has_infs" in finset_family
 
 variables {s t} {a b c : α}
 
-@[simp] lemma mem_infs : c ∈ s ⊼ t ↔ ∃ (a ∈ s) (b ∈ t), a ⊓ b = c := by simp [infs]
+@[simp] lemma mem_infs : c ∈ s ⊼ t ↔ ∃ (a ∈ s) (b ∈ t), a ⊓ b = c := by simp [(⊼)]
 
 variables (s t)
 
-@[simp, norm_cast] lemma coe_infs : (s ⊼ t : set α) = set.image2 (⊓) s t := coe_image₂ _ _ _
+@[simp, norm_cast] lemma coe_infs : (↑(s ⊼ t) : set α) = s ⊼ t := coe_image₂ _ _ _
 
 lemma card_infs_le : (s ⊼ t).card ≤ s.card * t.card := card_image₂_le _ _ _
 
@@ -141,29 +144,28 @@ lemma infs_subset : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ 
 lemma infs_subset_left : t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂ := image₂_subset_left
 lemma infs_subset_right : s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t := image₂_subset_right
 
-lemma image_subset_infs_left : b ∈ t → (λ a, a ⊓ b) '' s ⊆ s ⊼ t := image_subset_image₂_left
-lemma image_subset_infs_right : a ∈ s → (⊓) a '' t ⊆ s ⊼ t := image_subset_image₂_right
+lemma image_subset_infs_left : b ∈ t → s.image (λ a, a ⊓ b) ⊆ s ⊼ t := image_subset_image₂_left
+lemma image_subset_infs_right : a ∈ s → t.image ((⊓) a) ⊆ s ⊼ t := image_subset_image₂_right
 
 lemma forall_infs_iff {p : α → Prop} : (∀ c ∈ s ⊼ t, p c) ↔ ∀ (a ∈ s) (b ∈ t), p (a ⊓ b) :=
 forall_image₂_iff
 
 @[simp] lemma infs_subset_iff : s ⊼ t ⊆ u ↔ ∀ (a ∈ s) (b ∈ t), a ⊓ b ∈ u := image₂_subset_iff
 
-@[simp] lemma infs_nonempty_iff : (s ⊼ t).nonempty ↔ s.nonempty ∧ t.nonempty := image₂_nonempty_iff
+@[simp] lemma infs_nonempty : (s ⊼ t).nonempty ↔ s.nonempty ∧ t.nonempty := image₂_nonempty_iff
 
-lemma nonempty.infs : s.nonempty → t.nonempty → (s ⊼ t).nonempty := nonempty.image₂
+protected lemma nonempty.infs : s.nonempty → t.nonempty → (s ⊼ t).nonempty := nonempty.image₂
 lemma nonempty.of_infs_left : (s ⊼ t).nonempty → s.nonempty := nonempty.of_image₂_left
 lemma nonempty.of_infs_right : (s ⊼ t).nonempty → t.nonempty := nonempty.of_image₂_right
 
-@[simp] lemma infs_empty_left : ∅ ⊼ t = ∅ := image₂_empty_left
-@[simp] lemma infs_empty_right : s ⊼ ∅ = ∅ := image₂_empty_right
-@[simp] lemma infs_eq_empty_iff : s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅ := image₂_eq_empty_iff
+@[simp] lemma empty_infs : ∅ ⊼ t = ∅ := image₂_empty_left
+@[simp] lemma infs_empty : s ⊼ ∅ = ∅ := image₂_empty_right
+@[simp] lemma infs_eq_empty : s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅ := image₂_eq_empty_iff
 
-@[simp] lemma infs_singleton_left : {a} ⊼ t = t.image (λ b, a ⊓ b) := image₂_singleton_left
-@[simp] lemma infs_singleton_right : s ⊼ {b} = s.image (λ a, a ⊓ b) := image₂_singleton_right
-lemma infs_singleton_left' : {a} ⊼ t = t.image ((⊓) a) := image₂_singleton_left'
+@[simp] lemma singleton_infs : {a} ⊼ t = t.image (λ b, a ⊓ b) := image₂_singleton_left
+@[simp] lemma infs_singleton : s ⊼ {b} = s.image (λ a, a ⊓ b) := image₂_singleton_right
 
-lemma infs_singleton : ({a} ⊼ {b} : finset α) = {a ⊓ b} := image₂_singleton
+lemma singleton_infs_singleton : ({a} ⊼ {b} : finset α) = {a ⊓ b} := image₂_singleton
 
 lemma infs_union_left : (s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t := image₂_union_left
 lemma infs_union_right : s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂ := image₂_union_right
@@ -172,10 +174,10 @@ lemma infs_inter_subset_left : (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼
 lemma infs_inter_subset_right : s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂ := image₂_inter_subset_right
 
 lemma subset_infs {s t : set α} :
-  ↑u ⊆ set.image2 (⊓) s t → ∃ s' t' : finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t' :=
+  ↑u ⊆ s ⊼ t → ∃ s' t' : finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t' :=
 subset_image₂
 
-variables (s t u)
+variables (s t u v)
 
 lemma bUnion_image_inf_left : s.bUnion (λ a, t.image $ (⊓) a) = s ⊼ t := bUnion_image_left
 lemma bUnion_image_inf_right : t.bUnion (λ b, s.image $ λ a, a ⊓ b) = s ⊼ t := bUnion_image_right
@@ -187,11 +189,30 @@ lemma infs_assoc : (s ⊼ t) ⊼ u = s ⊼ (t ⊼ u) := image₂_assoc $ λ _ _
 lemma infs_comm : s ⊼ t = t ⊼ s := image₂_comm $ λ _ _, inf_comm
 lemma infs_left_comm : s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u) := image₂_left_comm inf_left_comm
 lemma infs_right_comm : (s ⊼ t) ⊼ u = (s ⊼ u) ⊼ t := image₂_right_comm inf_right_comm
+lemma infs_infs_infs_comm : (s ⊼ t) ⊼ (u ⊼ v) = (s ⊼ u) ⊼ (t ⊼ v) :=
+image₂_image₂_image₂_comm inf_inf_inf_comm
 
 end infs
 
 open_locale finset_family
 
+section distrib_lattice
+variables [distrib_lattice α] (s t u : finset α)
+
+lemma sups_infs_subset_left : s ⊻ (t ⊼ u) ⊆ (s ⊻ t) ⊼ (s ⊻ u) :=
+image₂_distrib_subset_left $ λ _ _ _, sup_inf_left
+
+lemma sups_infs_subset_right : (t ⊼ u) ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s) :=
+image₂_distrib_subset_right $ λ _ _ _, sup_inf_right
+
+lemma infs_sups_subset_left : s ⊼ (t ⊻ u) ⊆ (s ⊼ t) ⊻ (s ⊼ u) :=
+image₂_distrib_subset_left $ λ _ _ _, inf_sup_left
+
+lemma infs_sups_subset_right : (t ⊻ u) ⊼ s ⊆ (t ⊼ s) ⊻ (u ⊼ s) :=
+image₂_distrib_subset_right $ λ _ _ _, inf_sup_right
+
+end distrib_lattice
+
 section disj_sups
 variables [semilattice_sup α] [order_bot α] [@decidable_rel α disjoint]
   (s s₁ s₂ t t₁ t₂ u : finset α)
@@ -271,7 +292,7 @@ end disj_sups
 open_locale finset_family
 
 section distrib_lattice
-variables [distrib_lattice α] [order_bot α] [@decidable_rel α disjoint] (s t u : finset α)
+variables [distrib_lattice α] [order_bot α] [@decidable_rel α disjoint] (s t u v : finset α)
 
 lemma disj_sups_assoc : ∀ s t u : finset α, (s ○ t) ○ u = s ○ (t ○ u) :=
 begin
@@ -288,5 +309,8 @@ by simp_rw [←disj_sups_assoc, disj_sups_comm s]
 lemma disj_sups_right_comm : (s ○ t) ○ u = (s ○ u) ○ t :=
 by simp_rw [disj_sups_assoc, disj_sups_comm]
 
+lemma disj_sups_disj_sups_disj_sups_comm : (s ○ t) ○ (u ○ v) = (s ○ u) ○ (t ○ v) :=
+by simp_rw [←disj_sups_assoc, disj_sups_right_comm]
+
 end distrib_lattice
 end finset

src/data/set/n_ary.lean

@@ -26,8 +26,9 @@ and `set.image2` already fulfills this task.
 open function
 
 namespace set
-variables {α α' β β' γ γ' δ δ' ε ε' : Type*} {f f' : α → β → γ} {g g' : α → β → γ → δ}
-variables {s s' : set α} {t t' : set β} {u u' : set γ} {a a' : α} {b b' : β} {c c' : γ} {d d' : δ}
+variables {α α' β β' γ γ' δ δ' ε ε' ζ ζ' ν : Type*} {f f' : α → β → γ} {g g' : α → β → γ → δ}
+variables {s s' : set α} {t t' : set β} {u u' : set γ} {v : set δ} {a a' : α} {b b' : β} {c c' : γ}
+  {d d' : δ}
 
 
 /-- The image of a binary function `f : α → β → γ` as a function `set α → set β → set γ`.
@@ -235,6 +236,19 @@ lemma image2_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α 
   image2 f (image2 g s t) u = image2 g' (image2 f' s u) t :=
 by { rw [image2_swap g, image2_swap g'], exact image2_assoc (λ _ _ _, h_right_comm _ _ _) }
 
+lemma image2_image2_image2_comm {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν}
+  {g' : α → γ → ε'} {h' : β → δ → ζ'}
+  (h_comm : ∀ a b c d, f (g a b) (h c d) = f' (g' a c) (h' b d)) :
+  image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v) :=
+begin
+  ext,
+  split,
+  { rintro ⟨_, _, ⟨a, b, ha, hb, rfl⟩, ⟨c, d, hc, hd, rfl⟩, rfl⟩,
+    exact ⟨_, _, ⟨a, c, ha, hc, rfl⟩, ⟨b, d, hb, hd, rfl⟩, (h_comm _ _ _ _).symm⟩ },
+  { rintro ⟨_, _, ⟨a, c, ha, hc, rfl⟩, ⟨b, d, hb, hd, rfl⟩, rfl⟩,
+    exact ⟨_, _, ⟨a, b, ha, hb, rfl⟩, ⟨c, d, hc, hd, rfl⟩, h_comm _ _ _ _⟩ }
+end
+
 lemma image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
   (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
   (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) :=