-- Mathlib/Order/SupIndep.lean
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

Proof state:
case mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
⊢ ∀ ⦃i_1 : ι × ι'⦄, i_1 ∈ u → Disjoint (f (i, i')) (f i_1)

Tactic:
rintro ⟨j, j'⟩ hj

Result:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hj : (j, j') ∈ u
⊢ Disjoint (f (i, i')) (f (j, j'))

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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

Tactic:
rintro u hu ⟨i, i'⟩ hi hiu

Result:
case mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
⊢ Disjoint (f (i, i')) (u.sup f)

Proof state:
case mk.mk.inr.refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => t.sup fun i' => f (i, i')) (i, i').1

Tactic:
convert le_sup (α := α) hi.2

Result:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (i, i') = f ((i, i').1, (i, i').2)

Proof state:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j') ∈ s ×ˢ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
rw [mem_product] at hi hj

Result:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Proof state:
case mk.mk.inl
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ Disjoint (f (i, i')) (f (i, j'))

Tactic:
refine (ht.pairwiseDisjoint hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 hij).mono ?_ ?_

Result:
case mk.mk.inl.refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, i') ≤ (fun i' => s.sup fun i => f (i, i')) (i, i').2

case mk.mk.inl.refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, j') ≤ (fun i' => s.sup fun i => f (i, i')) (i, j').2

Proof state:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hj : (j, j') ∈ u
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
have hij := (ne_of_mem_of_not_mem hj hiu).symm

Result:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hj : (j, j') ∈ u
hij : (i, i') ≠ (j, j')
⊢ Disjoint (f (i, i')) (f (j, j'))

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (i, i') = f ((i, i').1, (i, i').2)

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.inl.refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, i') ≤ (fun i' => s.sup fun i => f (i, i')) (i, i').2

Tactic:
convert le_sup (α := α) hi.1

Result:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
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')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, i') = f ((i, i').1, (i, i').2)