∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (fst : α) (snd : β)
  (snd_1 : γ) (fst_1 : α) (snd_2 : β) (snd_3 : γ),
  (Equiv.prodAssoc α β γ) ((fst, snd), snd_1) ≤ (Equiv.prodAssoc α β γ) ((fst_1, snd_2), snd_3) ↔
    ((fst, snd), snd_1) ≤ ((fst_1, snd_2), snd_3)