[Merged by Bors] - feat: More sup_indep lemmas

Mathlib/Data/Finset/Pairwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finset.pairwise
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit c4c2ed622f43768eff32608d4a0f8a6cec1c047d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -40,13 +40,24 @@ theorem PairwiseDisjoint.elim_finset {s : Set ι} {f : ι → Finset α} (hs : s
   hs.elim hi hj (Finset.not_disjoint_iff.2 ⟨a, hai, haj⟩)
 #align set.pairwise_disjoint.elim_finset Set.PairwiseDisjoint.elim_finset
 
-theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] [SemilatticeInf α] [OrderBot α]
-    {s : Finset ι} {f : ι → α} (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι}
-    (hf : ∀ a, f (g a) ≤ f a) : (s.image g : Set ι).PairwiseDisjoint f := by
+section SemilatticeInf
+
+variable [SemilatticeInf α] [OrderBot α] {s : Finset ι} {f : ι → α}
+
+theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] {s : Finset ι} {f : ι → α}
+    (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι} (hf : ∀ a, f (g a) ≤ f a) :
+    (s.image g : Set ι).PairwiseDisjoint f := by
   rw [coe_image]
   exact hs.image_of_le hf
 #align set.pairwise_disjoint.image_finset_of_le Set.PairwiseDisjoint.image_finset_of_le
 
+theorem PairwiseDisjoint.attach (hs : (s : Set ι).PairwiseDisjoint f) :
+    (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val) := fun i _ j _ hij =>
+  hs i.2 j.2 <| mt Subtype.ext_val hij
+#align set.pairwise_disjoint.attach Set.PairwiseDisjoint.attach
+
+end SemilatticeInf
+
 variable [Lattice α] [OrderBot α]
 
 /-- Bind operation for `Set.PairwiseDisjoint`. In a complete lattice, you can use

Mathlib/Data/Set/Pairwise/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module data.set.pairwise.basic
-! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
+! leanprover-community/mathlib commit c4c2ed622f43768eff32608d4a0f8a6cec1c047d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -33,7 +33,7 @@ on `Set.PairwiseDisjoint`, even though the latter unfolds to something nicer.
 -/
 
 
-open Set Function
+open Function Order Set
 
 variable {α β γ ι ι' : Type _} {r p q : α → α → Prop}
 
@@ -345,6 +345,8 @@ end SemilatticeInfBot
 
 /-! ### Pairwise disjoint set of sets -/
 
+variable {s : Set ι} {t : Set ι'}
+
 theorem pairwiseDisjoint_range_singleton :
     (range (singleton : ι → Set ι)).PairwiseDisjoint id := by
   rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
@@ -361,6 +363,24 @@ theorem PairwiseDisjoint.elim_set {s : Set ι} {f : ι → Set α} (hs : s.Pairw
   hs.elim hi hj <| not_disjoint_iff.2 ⟨a, hai, haj⟩
 #align set.pairwise_disjoint.elim_set Set.PairwiseDisjoint.elim_set
 
+theorem PairwiseDisjoint.prod {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f)
+    (ht : t.PairwiseDisjoint g) :
+    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2 :=
+  fun ⟨_, _⟩ ⟨hi, hi'⟩ ⟨_, _⟩ ⟨hj, hj'⟩ hij =>
+  disjoint_left.2 fun ⟨_, _⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ =>
+    hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj
+#align set.pairwise_disjoint.prod Set.PairwiseDisjoint.prod
+
+theorem pairwiseDisjoint_pi {ι' α : ι → Type _} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)}
+    (hs : ∀ i, (s i).PairwiseDisjoint (f i)) :
+    ((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i) :=
+  fun _ hI _ hJ hIJ =>
+  disjoint_left.2 fun a haI haJ =>
+    hIJ <|
+      funext fun i =>
+        (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)
+#align set.pairwise_disjoint_pi Set.pairwiseDisjoint_pi
+
 /-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
 disjoint iff `f` is injective . -/
 theorem pairwiseDisjoint_image_right_iff {f : α → β → γ} {s : Set α} {t : Set β}

Mathlib/Data/Set/Pairwise/Lattice.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module data.set.pairwise.lattice
-! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
+! leanprover-community/mathlib commit c4c2ed622f43768eff32608d4a0f8a6cec1c047d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,17 +18,16 @@ In this file we prove many facts about `Pairwise` and the set lattice.
 -/
 
 
-open Set Function
-
-variable {α β γ ι ι' : Type _} {r p q : α → α → Prop}
+open Function Set Order
 
+variable {α β γ ι ι' : Type _} {κ : Sort _} {r p q : α → α → Prop}
 section Pairwise
 
 variable {f g : ι → α} {s t u : Set α} {a b : α}
 
 namespace Set
 
-theorem pairwise_iUnion {f : ι → Set α} (h : Directed (· ⊆ ·) f) :
+theorem pairwise_iUnion {f : κ → Set α} (h : Directed (· ⊆ ·) f) :
     (⋃ n, f n).Pairwise r ↔ ∀ n, (f n).Pairwise r := by
   constructor
   · intro H n
@@ -69,8 +68,7 @@ end PartialOrderBot
 
 section CompleteLattice
 
-variable [CompleteLattice α]
-
+variable [CompleteLattice α] {s : Set ι} {t : Set ι'}
 
 /-- Bind operation for `Set.PairwiseDisjoint`. If you want to only consider finsets of indices, you
 can use `Set.PairwiseDisjoint.biUnion_finset`. -/
@@ -89,8 +87,43 @@ theorem PairwiseDisjoint.biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι →
       (le_iSup₂ (f := fun i (_ : i ∈ g d) => f i) b hb)
 #align set.pairwise_disjoint.bUnion Set.PairwiseDisjoint.biUnion
 
+/-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
+pairwise disjoint. Not to be confused with `Set.PairwiseDisjoint.prod`. -/
+theorem PairwiseDisjoint.prod_left {f : ι × ι' → α}
+    (hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i'))
+    (ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) :
+    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f := by
+  rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h
+  rw [mem_prod] at hi hj
+  obtain rfl | hij := eq_or_ne i j
+  · refine' (ht hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 h).mono _ _
+    · convert le_iSup₂ (α := α) i hi.1; rfl
+    · convert le_iSup₂ (α := α) i hj.1; rfl
+  · refine' (hs hi.1 hj.1 hij).mono _ _
+    · convert le_iSup₂ (α := α) i' hi.2; rfl
+    · convert le_iSup₂ (α := α) j' hj.2; rfl
+#align set.pairwise_disjoint.prod_left Set.PairwiseDisjoint.prod_left
+
 end CompleteLattice
 
+section Frame
+
+variable [Frame α]
+
+theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' → α} :
+    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f ↔
+      (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧
+        t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i') := by
+  refine'
+        ⟨fun h => ⟨fun i hi j hj hij => _, fun i hi j hj hij => _⟩, fun h => h.1.prod_left h.2⟩ <;>
+      simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff] <;>
+    intro i' hi' j' hj'
+  · exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
+  · exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)
+#align set.pairwise_disjoint_prod_left Set.pairwiseDisjoint_prod_left
+
+end Frame
+
 theorem biUnion_diff_biUnion_eq {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) :
     ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) = ⋃ i ∈ s \ t, f i := by
   refine'

Mathlib/Data/Set/Prod.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Patrick Massot
 
 ! This file was ported from Lean 3 source module data.set.prod
-! leanprover-community/mathlib commit 27f315c5591c84687852f816d8ef31fe103d03de
+! leanprover-community/mathlib commit c4c2ed622f43768eff32608d4a0f8a6cec1c047d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -173,11 +173,22 @@ theorem prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×
   simp [and_assoc, and_left_comm]
 #align set.prod_inter_prod Set.prod_inter_prod
 
+@[simp]
 theorem disjoint_prod : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂ := by
   simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ←
     @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]
 #align set.disjoint_prod Set.disjoint_prod
 
+theorem Disjoint.set_prod_left (hs : Disjoint s₁ s₂) (t₁ t₂ : Set β) :
+    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
+  disjoint_left.2 fun ⟨_a, _b⟩ ⟨ha₁, _⟩ ⟨ha₂, _⟩ => disjoint_left.1 hs ha₁ ha₂
+#align set.disjoint.set_prod_left Set.Disjoint.set_prod_left
+
+theorem Disjoint.set_prod_right (ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) :
+    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
+  disjoint_left.2 fun ⟨_a, _b⟩ ⟨_, hb₁⟩ ⟨_, hb₂⟩ => disjoint_left.1 ht hb₁ hb₂
+#align set.disjoint.set_prod_right Set.Disjoint.set_prod_right
+
 theorem insert_prod : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t := by
   ext ⟨x, y⟩
   simp (config := { contextual := true }) [image, iff_def, or_imp, Imp.swap]
@@ -710,6 +721,24 @@ theorem disjoint_univ_pi : Disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Dis
   simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]
 #align set.disjoint_univ_pi Set.disjoint_univ_pi
 
+theorem Disjoint.set_pi (hi : i ∈ s) (ht : Disjoint (t₁ i) (t₂ i)) : Disjoint (s.pi t₁) (s.pi t₂) :=
+  disjoint_left.2 fun _ h₁ h₂ => disjoint_left.1 ht (h₁ _ hi) (h₂ _ hi)
+#align set.disjoint.set_pi Set.Disjoint.set_pi
+
+section Nonempty
+
+variable [∀ i, Nonempty (α i)]
+
+theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff]
+#align set.pi_eq_empty_iff' Set.pi_eq_empty_iff'
+
+@[simp]
+theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by
+  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']
+#align set.disjoint_pi Set.disjoint_pi
+
+end Nonempty
+
 -- Porting note: Removing `simp` - LHS does not simplify
 theorem range_dcomp (f : ∀ i, α i → β i) :
     (range fun g : ∀ i, α i => fun i => f i (g i)) = pi univ fun i => range (f i) := by

Mathlib/Order/SupIndep.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Kevin Buzzard, Yaël Dillies, Eric Wieser
 
 ! This file was ported from Lean 3 source module order.sup_indep
-! leanprover-community/mathlib commit 1c857a1f6798cb054be942199463c2cf904cb937
+! leanprover-community/mathlib commit c4c2ed622f43768eff32608d4a0f8a6cec1c047d
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Finset.Pairwise
 import Mathlib.Data.Finset.Powerset
 import Mathlib.Data.Fintype.Basic
@@ -89,13 +90,43 @@ theorem SupIndep.pairwiseDisjoint (hs : s.SupIndep f) : (s : Set ι).PairwiseDis
     sup_singleton.subst <| hs (singleton_subset_iff.2 hb) ha <| not_mem_singleton.2 hab
 #align finset.sup_indep.pairwise_disjoint Finset.SupIndep.pairwiseDisjoint
 
+theorem SupIndep.le_sup_iff (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) :
+    f i ≤ t.sup f ↔ i ∈ t := by
+  refine' ⟨fun h => _, le_sup⟩
+  by_contra hit
+  exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)
+#align finset.sup_indep.le_sup_iff Finset.SupIndep.le_sup_iff
+
 /-- The RHS looks like the definition of `CompleteLattice.Independent`. -/
 theorem supIndep_iff_disjoint_erase [DecidableEq ι] :
     s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f) :=
   ⟨fun hs _ hi => hs (erase_subset _ _) hi (not_mem_erase _ _), fun hs _ ht i hi hit =>
     (hs i hi).mono_right (sup_mono fun _ hj => mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩
 #align finset.sup_indep_iff_disjoint_erase Finset.supIndep_iff_disjoint_erase
 
+theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) :
+    (s.image g).SupIndep f := by
+  intro t ht i hi hit
+  rw [mem_image] at hi
+  obtain ⟨i, hi, rfl⟩ := hi
+  haveI : DecidableEq ι' := Classical.decEq _
+  suffices hts : t ⊆ (s.erase i).image g
+  · refine' (supIndep_iff_disjoint_erase.1 hs i hi).mono_right ((sup_mono hts).trans _)
+    rw [sup_image]
+  rintro j hjt
+  obtain ⟨j, hj, rfl⟩ := mem_image.1 (ht hjt)
+  exact mem_image_of_mem _ (mem_erase.2 ⟨ne_of_apply_ne g (ne_of_mem_of_not_mem hjt hit), hj⟩)
+#align finset.sup_indep.image Finset.SupIndep.image
+
+theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g) := by
+  refine' ⟨fun hs t ht i hi hit => _, fun hs => _⟩
+  · rw [← sup_map]
+    exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])
+  · classical
+    rw [map_eq_image]
+    exact hs.image
+#align finset.sup_indep_map Finset.supIndep_map
+
 @[simp]
 theorem supIndep_pair [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
     ({i, j} : Finset ι).SupIndep f ↔ Disjoint (f i) (f j) :=
@@ -131,16 +162,39 @@ theorem supIndep_univ_fin_two (f : Fin 2 → α) :
   supIndep_pair this
 #align finset.sup_indep_univ_fin_two Finset.supIndep_univ_fin_two
 
-theorem SupIndep.attach (hs : s.SupIndep f) : s.attach.SupIndep (f ∘ Subtype.val) := by
+theorem SupIndep.attach (hs : s.SupIndep f) : s.attach.SupIndep fun a => f a := by
   intro t _ i _ hi
   classical
-    rw [← Finset.sup_image]
+    have : (fun (a : { x // x ∈ s }) => f ↑a) = f ∘ (fun a : { x // x ∈ s } => ↑a) := rfl
+    rw [this, ← Finset.sup_image]
     refine' hs (image_subset_iff.2 fun (j : { x // x ∈ s }) _ => j.2) i.2 fun hi' => hi _
     rw [mem_image] at hi'
     obtain ⟨j, hj, hji⟩ := hi'
     rwa [Subtype.ext hji] at hj
 #align finset.sup_indep.attach Finset.SupIndep.attach
 
+/-
+Porting note: simpNF linter returns
+
+"Left-hand side does not simplify, when using the simp lemma on itself."
+
+However, simp does indeed solve the following. leanprover/std4#71 is related.
+
+example {α ι} [Lattice α] [OrderBot α] (s : Finset ι) (f : ι → α) :
+  (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := by simp
+-/
+@[simp, nolint simpNF]
+theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := by
+  refine' ⟨fun h t ht i his hit => _, SupIndep.attach⟩
+  classical
+  convert h (filter_subset (fun (i : { x // x ∈ s }) => (i : ι) ∈ t) _) (mem_attach _ ⟨i, ‹_›⟩)
+    fun hi => hit <| by simpa using hi using 1
+  refine' eq_of_forall_ge_iff _
+  simp only [Finset.sup_le_iff, mem_filter, mem_attach, true_and_iff, Function.comp_apply,
+    Subtype.forall, Subtype.coe_mk]
+  exact fun a => forall_congr' fun j => ⟨fun h _ => h, fun h hj => h (ht hj) hj⟩
+#align finset.sup_indep_attach Finset.supIndep_attach
+
 end Lattice
 
 section DistribLattice
@@ -173,6 +227,53 @@ theorem SupIndep.biUnion [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset 
   exact hs.sup hg
 #align finset.sup_indep.bUnion Finset.SupIndep.biUnion
 
+/-- Bind operation for `sup_indep`. -/
+theorem SupIndep.sigma {β : ι → Type _} {s : Finset ι} {g : ∀ i, Finset (β i)} {f : Sigma β → α}
+    (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩)
+    (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) : (s.sigma g).SupIndep f := by
+  rintro t ht ⟨i, b⟩ hi hit
+  rw [Finset.disjoint_sup_right]
+  rintro ⟨j, c⟩ hj
+  have hbc := (ne_of_mem_of_not_mem hj hit).symm
+  replace hj := ht hj
+  rw [mem_sigma] at hi hj
+  obtain rfl | hij := eq_or_ne i j
+  · exact (hg _ hj.1).pairwiseDisjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc)
+  · refine' (hs.pairwiseDisjoint hi.1 hj.1 hij).mono _ _
+    · convert le_sup (α := α) hi.2; simp
+    · convert le_sup (α := α) hj.2; simp
+#align finset.sup_indep.sigma Finset.SupIndep.sigma
+
+theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α}
+    (hs : s.SupIndep fun i => t.sup fun i' => f (i, i'))
+    (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f := by
+  rintro u hu ⟨i, i'⟩ hi hiu
+  rw [Finset.disjoint_sup_right]
+  rintro ⟨j, j'⟩ hj
+  have hij := (ne_of_mem_of_not_mem hj hiu).symm
+  replace hj := hu hj
+  rw [mem_product] at hi hj
+  obtain rfl | hij := eq_or_ne i j
+  · refine' (ht.pairwiseDisjoint hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 hij).mono _ _
+    · convert le_sup (α := α) hi.1; simp
+    · convert le_sup (α := α) hj.1; simp
+  · refine' (hs.pairwiseDisjoint hi.1 hj.1 hij).mono _ _
+    · convert le_sup (α := α) hi.2; simp
+    · convert le_sup (α := α) hj.2; simp
+#align finset.sup_indep.product Finset.SupIndep.product
+
+theorem supIndep_product_iff {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} :
+    (s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i'))
+      ∧ t.SupIndep fun i' => s.sup fun i => f (i, i') := by
+  refine' ⟨_, fun h => h.1.product h.2⟩
+  simp_rw [supIndep_iff_pairwiseDisjoint]
+  refine' fun h => ⟨fun i hi j hj hij => _, fun i hi j hj hij => _⟩ <;>
+      simp_rw [Function.onFun, Finset.disjoint_sup_left, Finset.disjoint_sup_right] <;>
+    intro i' hi' j' hj'
+  · exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij)
+  · exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij)
+#align finset.sup_indep_product_iff Finset.supIndep_product_iff
+
 end DistribLattice
 
 end Finset