no goals
ι : Type u_2
α' : ι → Type u_1
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]