∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ},
  ψ ∘ φ = ρ ∘ θ → ∀ (G : Filter δ), Filter.comap φ (Filter.comap ψ G) = Filter.comap θ (Filter.comap ρ G)